# HG changeset patch
# User wenzelm
# Date 1319662266 -7200
# Node ID 6f8949e6c71a9c7bf95f1a8c88492426f80a1ffd
# Parent  a42624e9de091586883a67a5a7d89d02a75a71bb
more robust ML pretty printing (cf. b6c527c64789);

diff -r a42624e9de09 -r 6f8949e6c71a src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Oct 26 22:50:40 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Oct 26 22:51:06 2011 +0200
@@ -31,9 +31,14 @@
     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
   else Pretty.str "<context>");
 
-fun default_context thy =
-  Context.cases Syntax.init_pretty_global I
-    (the_default (Context.Theory thy) (try ML_Context.the_generic_context ()));
+fun default_context thy0 =
+  (case Context.thread_data () of
+    SOME (Context.Proof ctxt) => ctxt
+  | SOME (Context.Theory thy) =>
+      (case try Syntax.init_pretty_global thy of
+        SOME ctxt => ctxt
+      | NONE => Syntax.init_pretty_global thy0)
+  | NONE => Syntax.init_pretty_global thy0);
 
 fun pp_thm th =
   let