top_function_of
top_function_of : hol_error -> string
Extract last function name added to a hol_error.
An invocation top_function_of holerr returns the function name of
the top origin element held in holerr.
Example
> top_function_of
(mk_hol_error "Foo" "bar" locn.Loc_Unknown "bad input")
val it = "bar": string
Failure
The call fails if the origin stack of the hol_error is empty.
See also
Feedback,
Feedback.mk_hol_error,
Feedback.origins_of,
Feedback.message_of,
Feedback.top_structure_of,
Feedback.top_location_of,
Feedback.set_top_function