src/Pure/Isar/proof_display.ML

--- a/src/Pure/Isar/proof_display.ML	Wed Mar 26 22:40:05 2008 +0100
+++ b/src/Pure/Isar/proof_display.ML	Wed Mar 26 22:40:07 2008 +0100
@@ -123,7 +123,7 @@
 fun present_results ctxt ((kind, name), res) =
   if kind = "" orelse kind = Thm.internalK then ()
   else (print_results true ctxt ((kind, name), res);
-    ML_Context.setmp (SOME (Context.Proof ctxt))
+    Context.setmp_thread_data (SOME (Context.Proof ctxt))
       (Present.results kind) (name_results name res));
 
 end;