--- a/src/ZF/ind_syntax.ML Sun Sep 12 17:39:02 2010 +0200
+++ b/src/ZF/ind_syntax.ML Sun Sep 12 19:04:02 2010 +0200
@@ -66,7 +66,7 @@
(*read a constructor specification*)
fun read_construct ctxt (id: string, sprems, syn: mixfix) =
- let val prems = map (Syntax.parse_term ctxt #> Type_Infer.constrain FOLogic.oT) sprems
+ let val prems = map (Syntax.parse_term ctxt #> Type.constraint FOLogic.oT) sprems
|> Syntax.check_terms ctxt
val args = map (#1 o dest_mem) prems
val T = (map (#2 o dest_Free) args) ---> iT