src/HOL/Tools/inductive_package.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15703 727ef1b8b3ee
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -183,8 +183,8 @@
     1.4      fun varify (t, (i, ts)) =
     1.5        let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
     1.6        in (maxidx_of_term t', t'::ts) end;
     1.7 -    val (i, cs') = Library.foldr varify (cs, (~1, []));
     1.8 -    val (i', intr_ts') = Library.foldr varify (intr_ts, (i, []));
     1.9 +    val (i, cs') = foldr varify (~1, []) cs;
    1.10 +    val (i', intr_ts') = foldr varify (i, []) intr_ts;
    1.11      val rec_consts = Library.foldl add_term_consts_2 ([], cs');
    1.12      val intr_consts = Library.foldl add_term_consts_2 ([], intr_ts');
    1.13      fun unify (env, (cname, cT)) =
    1.14 @@ -271,12 +271,12 @@
    1.15  
    1.16  val remove_split = rewrite_rule [split_conv RS eq_reflection];
    1.17  
    1.18 -fun split_rule_vars vs rl = standard (remove_split (Library.foldr split_rule_var'
    1.19 -  (mg_prod_factors vs ([], Thm.prop_of rl), rl)));
    1.20 +fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
    1.21 +  rl (mg_prod_factors vs ([], Thm.prop_of rl))));
    1.22  
    1.23 -fun split_rule vs rl = standard (remove_split (Library.foldr split_rule_var'
    1.24 -  (List.mapPartial (fn (t as Var ((a, _), _)) =>
    1.25 -    Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)), rl)));
    1.26 +fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
    1.27 +  rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
    1.28 +      Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)))));
    1.29  
    1.30  
    1.31  (** process rules **)
    1.32 @@ -337,7 +337,7 @@
    1.33  
    1.34  fun mk_elims cs cTs params intr_ts intr_names =
    1.35    let
    1.36 -    val used = Library.foldr add_term_names (intr_ts, []);
    1.37 +    val used = foldr add_term_names [] intr_ts;
    1.38      val [aname, pname] = variantlist (["a", "P"], used);
    1.39      val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
    1.40  
    1.41 @@ -353,7 +353,7 @@
    1.42          val a = Free (aname, T);
    1.43  
    1.44          fun mk_elim_prem (_, t, ts) =
    1.45 -          list_all_free (map dest_Free ((Library.foldr add_term_frees (t::ts, [])) \\ params),
    1.46 +          list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params),
    1.47              Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
    1.48          val c_intrs = (List.filter (equal c o #1 o #1) intrs);
    1.49        in
    1.50 @@ -369,7 +369,7 @@
    1.51  
    1.52  fun mk_indrule cs cTs params intr_ts =
    1.53    let
    1.54 -    val used = Library.foldr add_term_names (intr_ts, []);
    1.55 +    val used = foldr add_term_names [] intr_ts;
    1.56  
    1.57      (* predicates for induction rule *)
    1.58  
    1.59 @@ -407,8 +407,8 @@
    1.60            HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
    1.61  
    1.62        in list_all_free (frees,
    1.63 -           Logic.list_implies (map HOLogic.mk_Trueprop (Library.foldr mk_prem
    1.64 -             (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
    1.65 +           Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
    1.66 +             [] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))),
    1.67                 HOLogic.mk_Trueprop (valOf (pred_of u) $ t)))
    1.68        end;
    1.69  
    1.70 @@ -422,15 +422,15 @@
    1.71        let val T = HOLogic.dest_setT (fastype_of c);
    1.72            val ps = getOpt (assoc (factors, P), []);
    1.73            val Ts = prodT_factors [] ps T;
    1.74 -          val (frees, x') = Library.foldr (fn (T', (fs, s)) =>
    1.75 -            ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
    1.76 +          val (frees, x') = foldr (fn (T', (fs, s)) =>
    1.77 +            ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
    1.78            val tuple = mk_tuple [] ps T frees;
    1.79        in ((HOLogic.mk_binop "op -->"
    1.80          (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
    1.81        end;
    1.82  
    1.83      val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
    1.84 -        (fst (Library.foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
    1.85 +        (fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds))))
    1.86  
    1.87    in (preds, ind_prems, mutual_ind_concl,
    1.88      map (apfst (fst o dest_Free)) factors)
    1.89 @@ -707,7 +707,7 @@
    1.90  
    1.91      val fp_name = if coind then gfp_name else lfp_name;
    1.92  
    1.93 -    val used = Library.foldr add_term_names (intr_ts, []);
    1.94 +    val used = foldr add_term_names [] intr_ts;
    1.95      val [sname, xname] = variantlist (["S", "x"], used);
    1.96  
    1.97      (* transform an introduction rule into a conjunction  *)
    1.98 @@ -723,11 +723,11 @@
    1.99          val Const ("op :", _) $ t $ u =
   1.100            HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   1.101  
   1.102 -      in Library.foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   1.103 -        (frees, foldr1 HOLogic.mk_conj
   1.104 +      in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   1.105 +        (foldr1 HOLogic.mk_conj
   1.106            (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   1.107              (map (subst o HOLogic.dest_Trueprop)
   1.108 -              (Logic.strip_imp_prems r))))
   1.109 +              (Logic.strip_imp_prems r)))) frees
   1.110        end
   1.111  
   1.112      (* make a disjunction of all introduction rules *)