more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);

--- a/src/Pure/Isar/runtime.ML	Wed Oct 19 15:42:43 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Oct 19 16:45:46 2011 +0200
@@ -126,8 +126,11 @@
     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);
+        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);
       in raise TOPLEVEL_ERROR end;
 
 end;