--- a/src/HOL/Tools/inductive_package.ML Thu Jul 28 15:19:48 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu Jul 28 15:19:49 2005 +0200
@@ -177,7 +177,6 @@
same type in all introduction rules*)
fun unify_consts thy cs intr_ts =
(let
- val tsig = Sign.tsig_of thy;
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
fun varify (t, (i, ts)) =
let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
@@ -186,12 +185,10 @@
val (i', intr_ts') = foldr varify (i, []) intr_ts;
val rec_consts = fold add_term_consts_2 cs' [];
val intr_consts = fold add_term_consts_2 intr_ts' [];
- fun unify (env, (cname, cT)) =
+ fun unify (cname, cT) =
let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
- in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
- (env, (replicate (length consts) cT) ~~ consts)
- end;
- val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
+ in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
+ val (env, _) = fold unify rec_consts (Vartab.empty, i');
val subst = Type.freeze o map_term_types (Envir.norm_type env)
in (map subst cs', map subst intr_ts')