src/HOL/Tools/inductive_package.ML
changeset 17485 c39871c52977
parent 17412 e26cb20ef0cc
child 17959 8db36a108213
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Sep 19 15:12:13 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Sep 19 16:38:35 2005 +0200
     1.3 @@ -228,12 +228,12 @@
     1.4        p :: prod_factors (1::p) t @ prod_factors (2::p) u
     1.5    | prod_factors p _ = [];
     1.6  
     1.7 -fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
     1.8 +fun mg_prod_factors ts (t $ u) fs = if t mem ts then
     1.9          let val f = prod_factors [] u
    1.10          in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
    1.11 -      else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
    1.12 -  | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
    1.13 -  | mg_prod_factors ts (fs, _) = fs;
    1.14 +      else mg_prod_factors ts u (mg_prod_factors ts t fs)
    1.15 +  | mg_prod_factors ts (Abs (_, _, t)) fs = mg_prod_factors ts t fs
    1.16 +  | mg_prod_factors ts _ fs = fs;
    1.17  
    1.18  fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
    1.19        if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
    1.20 @@ -265,11 +265,11 @@
    1.21  val remove_split = rewrite_rule [split_conv RS eq_reflection];
    1.22  
    1.23  fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
    1.24 -  rl (mg_prod_factors vs ([], Thm.prop_of rl))));
    1.25 +  rl (mg_prod_factors vs (Thm.prop_of rl) [])));
    1.26  
    1.27  fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
    1.28    rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
    1.29 -      Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)))));
    1.30 +      Option.map (pair t) (AList.lookup (op =) vs a)) (term_vars (Thm.prop_of rl)))));
    1.31  
    1.32  
    1.33  (** process rules **)
    1.34 @@ -377,7 +377,7 @@
    1.35        let
    1.36          val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
    1.37  
    1.38 -        val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
    1.39 +        val pred_of = AList.lookup (op aconv) (cs ~~ preds);
    1.40  
    1.41          fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
    1.42                (case pred_of u of
    1.43 @@ -408,13 +408,13 @@
    1.44  
    1.45      val ind_prems = map mk_ind_prem intr_ts;
    1.46  
    1.47 -    val factors = Library.foldl (mg_prod_factors preds) ([], ind_prems);
    1.48 +    val factors = Library.fold (mg_prod_factors preds) ind_prems [];
    1.49  
    1.50      (* make conclusions for induction rules *)
    1.51  
    1.52      fun mk_ind_concl ((c, P), (ts, x)) =
    1.53        let val T = HOLogic.dest_setT (fastype_of c);
    1.54 -          val ps = getOpt (assoc (factors, P), []);
    1.55 +          val ps = AList.lookup (op =) factors P |> the_default [];
    1.56            val Ts = prodT_factors [] ps T;
    1.57            val (frees, x') = foldr (fn (T', (fs, s)) =>
    1.58              ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;