# HG changeset patch
# User wenzelm
# Date 1213821124 -7200
# Node ID 49c81f6d7a0860d0a581994c5bc78f188d7bba8a
# Parent  843472ae2116f5c514423efa2f18e27046f101dd
TypeExt.type_constraint;

diff -r 843472ae2116 -r 49c81f6d7a08 src/Pure/Syntax/syntax.ML
--- 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;