trye : ('a -> 'b) -> 'a -> 'b
The application trye f x evaluates f x; if this evaluates to y, then y is returned. However, if evaluation raises an exception e, there are three cases: if e is Interrupt, then it is raised; if e is HOL_ERR, then it is raised; otherwise, e is mapped to an application of HOL_ERR and then raised.
- hd ; ! Uncaught exception: ! Empty - trye hd ; ! Uncaught exception: ! HOL_ERR - trye (fn _ => raise Interrupt) 1; > Interrupted