src/Pure/Isar/proof_display.ML
changeset 22086 cf6019fece63
parent 21437 a3c55b85cf0e
child 22095 07875394618e
     1.1 --- a/src/Pure/Isar/proof_display.ML	Fri Jan 19 13:09:32 2007 +0100
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Fri Jan 19 13:09:33 2007 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4  fun present_results ctxt ((kind, name), res) =
     1.5    if kind = "" orelse kind = Thm.internalK then ()
     1.6    else (print_results true ctxt ((kind, name), res);
     1.7 -    Context.setmp (SOME (ProofContext.theory_of ctxt))
     1.8 +    Context.setmp (SOME (Context.Proof ctxt))
     1.9        (Present.results kind) (name_results name res));
    1.10  
    1.11  end;