| changeset 14287 | f630017ed01c |
| parent 14257 | a7ef3f7588c5 |
| child 14508 | 859b11514537 |
--- a/src/Pure/Isar/proof_context.ML Wed Dec 10 14:29:05 2003 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Dec 10 14:29:44 2003 +0100 @@ -421,6 +421,8 @@ in +(* Read/certify type, using default sort information from context. *) + val read_typ = read_typ_aux Sign.read_typ'; val read_typ_no_norm = read_typ_aux Sign.read_typ_no_norm'; val cert_typ = cert_typ_aux Sign.certify_typ;