# HG changeset patch
# User wenzelm
# Date 1406217846 -7200
# Node ID 88b52244574df91b0f7d0e6d876176eedb7425f9
# Parent  4b247a7586c92324bf4746a3ad760822129f2135
adhoc workaround to avoid hard crash after ML exception;

diff -r 4b247a7586c9 -r 88b52244574d src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Jul 24 17:58:29 2014 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Jul 24 18:04:06 2014 +0200
@@ -153,11 +153,7 @@
     if Exn.is_interrupt exn then reraise exn
     else
       let
-        val opt_ctxt =
-          (case Context.thread_data () of
-            NONE => NONE
-          | SOME context => try Context.proof_of context);
-        val _ = output_exn (exn_context opt_ctxt exn);
+        val _ = output_exn (exn_context NONE exn);
       in raise TOPLEVEL_ERROR end;
 
 fun toplevel_program body =