diff -r ca02a2077955 -r f137c5e971f5 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/Isar/proof_display.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -65,7 +65,7 @@
   | print_results false = K (K ());
 
 fun present_results ctxt ((kind, name), res) =
-  if kind = "" orelse kind = Drule.internalK then ()
+  if kind = "" orelse kind = PureThy.internalK then ()
   else (print_results true ctxt ((kind, name), res);
     Context.setmp (SOME (ProofContext.theory_of ctxt))
       (Present.results kind) (name_results name res));