# HG changeset patch
# User wenzelm
# Date 1406236646 -7200
# Node ID 1c0ee733325f74493e4fa5dd29170a4b2275aa9a
# Parent  179b9c43fe84b4cd761dca25204c27561706c23f
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;

diff -r 179b9c43fe84 -r 1c0ee733325f src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Jul 24 20:21:59 2014 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Jul 24 23:17:26 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;