author | wenzelm |
Wed, 18 Jun 2008 22:32:04 +0200 | |
changeset 27265 | 49c81f6d7a08 |
parent 27264 | 843472ae2116 |
child 27266 | a2db1e379778 |
--- 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;