(corrected wrong commit)
authorhaftmann
Wed Jul 13 10:48:21 2005 +0200 (2005-07-13)
changeset 1678654b5df610651
parent 16785 2eddcce4fd16
child 16787 b6b6e2faaa41
(corrected wrong commit)
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jul 13 10:44:51 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jul 13 10:48:21 2005 +0200
     1.3 @@ -178,8 +178,8 @@
     1.4  fun unify_consts thy cs intr_ts =
     1.5    (let
     1.6      val tsig = Sign.tsig_of thy;
     1.7 -    fun add_term_consts_2 (x, y) =
     1.8 -      fold_aterms (fn (Const c) => curry (op ins) c | _ => I) y x;
     1.9 +    val add_term_consts_2 =
    1.10 +      foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
    1.11      fun varify (t, (i, ts)) =
    1.12        let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
    1.13        in (maxidx_of_term t', t'::ts) end;