error_record
Feedback.type error_record = {origin_structure : string,
origin_function : string,
message : string}
Type abbreviation for HOL exceptions in Feedback module.
The type abbreviation error_record declares the standard format of HOL
exceptions. The origin_structure field denotes the module that the
exception has been raised in, the origin_function field gives the name
of the function the exception has been raised in, and the message
field should give an explanation of why the exception has been raised.
See also
Feedback, Feedback.HOL_ERR,
Feedback.format_ERR,
Feedback.ERR_to_string