| changeset 19391 | 4812d28c90a6 |
| parent 19305 | 5c16895d548b |
| child 19473 | d87a8838afa4 |
--- a/src/Pure/Proof/proof_syntax.ML Sun Apr 09 19:41:30 2006 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Mon Apr 10 00:33:49 2006 +0200 @@ -181,7 +181,7 @@ val MinProoft = Const ("MinProof", proofT); val mk_tyapp = Library.foldl (fn (prf, T) => Const ("Appt", - [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T); + [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); fun term_of _ (PThm ((name, _), _, _, NONE)) = Const (NameSpace.append "thm" name, proofT)