| changeset 27265 | 49c81f6d7a08 |
| parent 27195 | bbf4cbc69243 |
| child 27768 | 398c64b2acef |
--- a/src/Pure/Syntax/syntax.ML Wed Jun 18 22:32:03 2008 +0200 +++ b/src/Pure/Syntax/syntax.ML Wed Jun 18 22:32:04 2008 +0200 @@ -776,7 +776,7 @@ val check_typs = gen_check fst false; val check_terms = gen_check snd false; -fun check_props ctxt = map (TypeInfer.constrain propT) #> check_terms ctxt; +fun check_props ctxt = map (TypeExt.type_constraint propT) #> check_terms ctxt; val check_typ = singleton o check_typs; val check_term = singleton o check_terms;