controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;

--- a/src/Pure/Isar/toplevel.ML	Tue Mar 10 21:20:01 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Mar 10 21:43:19 2009 +0100
@@ -293,7 +293,10 @@
 local
 
 fun debugging f x =
-  if ! debug then exception_trace (fn () => f x)
+  if ! debug then
+    (case exception_trace (fn () => SOME (f x) handle UNDEF => NONE) of
+      SOME y => y
+    | NONE => raise UNDEF)
   else f x;
 
 fun toplevel_error f x =