src/Pure/Isar/proof_display.ML
changeset 21437 a3c55b85cf0e
parent 20889 f625a65bfed5
child 22086 cf6019fece63
     1.1 --- a/src/Pure/Isar/proof_display.ML	Tue Nov 21 18:07:32 2006 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Nov 21 18:07:33 2006 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4    | print_results false = K (K ());
     1.5  
     1.6  fun present_results ctxt ((kind, name), res) =
     1.7 -  if kind = "" orelse kind = PureThy.internalK then ()
     1.8 +  if kind = "" orelse kind = Thm.internalK then ()
     1.9    else (print_results true ctxt ((kind, name), res);
    1.10      Context.setmp (SOME (ProofContext.theory_of ctxt))
    1.11        (Present.results kind) (name_results name res));