ERR_to_string : (error_record -> string) ref
STRUCTURE
SYNOPSIS
Alterable function for formatting HOL_ERR.
DESCRIPTION
ERR_to_string is a reference to a function for formatting the argument to an application of HOL_ERR. It can be used to customize Raise.

The default value of ERR_to_string is format_ERR.

EXAMPLE
- fun alt_ERR_report {origin_structure,origin_function,message} =
     String.concat["This just in from ",origin_function, " at ",
                   origin_structure, " : ", message, "\n"];

- ERR_to_string := alt_ERR_report;

- Raise (HOL_ERR {origin_structure = "Foo",
                  origin_function = "bar",
                  message = "incomprehensible input"});

This just in from bar at Foo : incomprehensible input
! Uncaught exception:
! HOL_ERR

SEEALSO
HOL  Trindemossen-1