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