src/ZF/Tools/inductive_package.ML
changeset 37145 01aa36932739
parent 36960 01594f816e3a
child 37781 2fbbf0a48cef
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -555,7 +555,7 @@
     1.4      (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
     1.5    let
     1.6      val ctxt = ProofContext.init_global thy;
     1.7 -    val read_terms = map (Syntax.parse_term ctxt #> TypeInfer.constrain Ind_Syntax.iT)
     1.8 +    val read_terms = map (Syntax.parse_term ctxt #> Type_Infer.constrain Ind_Syntax.iT)
     1.9        #> Syntax.check_terms ctxt;
    1.10  
    1.11      val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;