theory Tracing_Example
  imports Pure
begin


ML \<open>

(* Raises exception Empty eventually. Recursive to avoid inlining. *)
fun f xs = case xs of _::xs' => f xs' | _ => hd xs;

(* Returns the empty list. Recursive to avoid inlining. *)
fun g xs = case xs of _::xs' => g xs' | _ => xs;

(* Would expect to see which function raises the exception, but I only get

  exception Empty raised (line 47 of "./basis/List.sml")

which does not help. *)
Runtime.exn_trace (fn () => (f [0,1], g [2,3]))
\<close>

end