1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 11 20:42:16 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 11 20:54:03 2009 +0100
     1.3 @@ -294,9 +294,10 @@
     1.4  
     1.5  fun debugging f x =
     1.6    if ! debug then
     1.7 -    (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of
     1.8 -      SOME y => y
     1.9 -    | NONE => raise UNDEF)
    1.10 +    Exn.release (exception_trace (fn () =>
    1.11 +      Exn.Result (f x) handle
    1.12 +        exn as UNDEF => Exn.Exn exn
    1.13 +      | exn as EXCURSION_FAIL _ => Exn.Exn exn))
    1.14    else f x;
    1.15  
    1.16  fun toplevel_error f x =