# HG changeset patch
# User blanchet
# Date 1406287357 -7200
# Node ID 2f46999395e233f42f1d7d943ba5eee1a2b1d1c8
# Parent  9bfa4cb2fee6f5feecb98f47f39ba1c90ed83d84# Parent  0c267a7a23f2b75216049431ddff26d058b9fed5
merge

diff -r 9bfa4cb2fee6 -r 2f46999395e2 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Fri Jul 25 13:15:50 2014 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Jul 25 13:22:37 2014 +0200
@@ -166,10 +166,10 @@
 (*Proof General legacy*)
 fun thread interrupts body =
   Thread.fork
-    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
-        |> debugging NONE
-        |> toplevel_error
-          (fn exn => Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn))),
+    (fn () =>
+      debugging NONE body () handle exn =>
+        if Exn.is_interrupt exn then ()
+        else Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn),
       Simple_Thread.attributes interrupts);
 
 end;