diff -r be1acdcd55dc -r 7189a138dd6c src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Sep 09 18:18:34 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Sep 09 18:21:06 2010 +0200
@@ -110,9 +110,14 @@
   |> debugging
   |> Future.interruptible_task;
 
-fun toplevel_error output_exn f x =
-  let val ctxt = Option.map Context.proof_of (Context.thread_data ())
-  in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end;
+fun toplevel_error output_exn f x = f x
+  handle exn =>
+    if Exn.is_interrupt exn then reraise exn
+    else
+      let
+        val ctxt = Option.map Context.proof_of (Context.thread_data ());
+        val _ = output_exn (exn_context ctxt exn);
+      in raise TOPLEVEL_ERROR end;
 
 end;