--- a/src/ZF/Tools/inductive_package.ML Thu May 27 15:28:23 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML Thu May 27 17:41:27 2010 +0200
@@ -555,7 +555,7 @@
(raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
let
val ctxt = ProofContext.init_global thy;
- val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
+ val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
#> Syntax.check_terms ctxt;
val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;