merged

--- a/src/Pure/Isar/proof_display.ML	Thu Oct 27 07:46:57 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Oct 27 07:48:07 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

--- a/src/Tools/Code/code_runtime.ML	Thu Oct 27 07:46:57 2011 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Oct 27 07:48:07 2011 +0200
@@ -422,7 +422,7 @@
     val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
     val _ = Secure.use_text notifying_context
       (0, Path.implode filepath) false (File.read filepath);
-    val thy'' = (Context.the_theory o the) (Context.thread_data ());
+    val thy'' = Context.the_theory (Context.the_thread_data ());
     val names = Loaded_Values.get thy'';
   in (names, thy'') end;