1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Mar 10 21:20:01 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Mar 10 21:43:19 2009 +0100
     1.3 @@ -293,7 +293,10 @@
     1.4  local
     1.5  
     1.6  fun debugging f x =
     1.7 -  if ! debug then exception_trace (fn () => f x)
     1.8 +  if ! debug then
     1.9 +    (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of
    1.10 +      SOME y => y
    1.11 +    | NONE => raise UNDEF)
    1.12    else f x;
    1.13  
    1.14  fun toplevel_error f x =