message_of
message_of : hol_error -> string
Extract message from a hol_error.
An invocation message_of holerr returns the message component of holerr.
Example
> message_of (mk_hol_error "Foo" "bar" locn.Loc_Unknown "bad input");
val it = "bad input": string
Failure
Never fails.
See also
Feedback,
Feedback.mk_hol_error,
Feedback.origins_of,
Feedback.top_structure_of,
Feedback.top_function_of