src/HOL/Tools/inductive_package.ML
changeset 16934 9ef19e3c7fdd
parent 16876 f57b38cced32
child 16975 34ed8d5d4f16
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Jul 28 15:19:48 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Jul 28 15:19:49 2005 +0200
     1.3 @@ -177,7 +177,6 @@
     1.4    same type in all introduction rules*)
     1.5  fun unify_consts thy cs intr_ts =
     1.6    (let
     1.7 -    val tsig = Sign.tsig_of thy;
     1.8      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     1.9      fun varify (t, (i, ts)) =
    1.10        let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
    1.11 @@ -186,12 +185,10 @@
    1.12      val (i', intr_ts') = foldr varify (i, []) intr_ts;
    1.13      val rec_consts = fold add_term_consts_2 cs' [];
    1.14      val intr_consts = fold add_term_consts_2 intr_ts' [];
    1.15 -    fun unify (env, (cname, cT)) =
    1.16 +    fun unify (cname, cT) =
    1.17        let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
    1.18 -      in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
    1.19 -          (env, (replicate (length consts) cT) ~~ consts)
    1.20 -      end;
    1.21 -    val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
    1.22 +      in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
    1.23 +    val (env, _) = fold unify rec_consts (Vartab.empty, i');
    1.24      val subst = Type.freeze o map_term_types (Envir.norm_type env)
    1.25  
    1.26    in (map subst cs', map subst intr_ts')