src/HOL/Tools/inductive_package.ML
changeset 16861 7446b4be013b
parent 16786 54b5df610651
child 16876 f57b38cced32
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 15 15:44:11 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 15 15:44:15 2005 +0200
     1.3 @@ -178,15 +178,14 @@
     1.4  fun unify_consts thy cs intr_ts =
     1.5    (let
     1.6      val tsig = Sign.tsig_of thy;
     1.7 -    val add_term_consts_2 =
     1.8 -      foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
     1.9 +    val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
    1.10      fun varify (t, (i, ts)) =
    1.11        let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
    1.12        in (maxidx_of_term t', t'::ts) end;
    1.13      val (i, cs') = foldr varify (~1, []) cs;
    1.14      val (i', intr_ts') = foldr varify (i, []) intr_ts;
    1.15 -    val rec_consts = Library.foldl add_term_consts_2 ([], cs');
    1.16 -    val intr_consts = Library.foldl add_term_consts_2 ([], intr_ts');
    1.17 +    val rec_consts = fold add_term_consts_2 cs' [];
    1.18 +    val intr_consts = fold add_term_consts_2 intr_ts' [];
    1.19      fun unify (env, (cname, cT)) =
    1.20        let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
    1.21        in Library.foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))