src/Pure/Isar/proof_display.ML

--- a/src/Pure/Isar/proof_display.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Isar/proof_display.ML	Fri Jan 19 13:09:33 2007 +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);
-    Context.setmp (SOME (ProofContext.theory_of ctxt))
+    Context.setmp (SOME (Context.Proof ctxt))
       (Present.results kind) (name_results name res));
 
 end;