format_ERR : error_record -> string
STRUCTURE
Feedback
SYNOPSIS
Maps argument record of HOL_ERR to a string.
DESCRIPTION
The format_ERR function maps the argument of an application of HOL_ERR to a string. It is the default function used by ERR_to_string.
FAILURE
Never fails.
EXAMPLE
- print
   (format_ERR {origin_structure = "Foo",
                origin_function = "bar",
                message = "incomprehensible input"});

Exception raised at Foo.bar:
incomprehensible input
> val it = () : unit

SEEALSO
Feedback, ERR_to_string, format_MESG, format_WARNING
HOL  Kananaskis-10