Datatype.read_typ: standard argument order;
authorwenzelm
Tue Oct 27 22:55:27 2009 +0100 (2009-10-27 ago)
changeset 33244db230399f890
parent 33243 17014b1b9353
child 33245 65232054ffd0
Datatype.read_typ: standard argument order;
eliminated some old folds;
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/recfun_codegen.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Oct 27 17:34:00 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Oct 27 22:55:27 2009 +0100
     1.3 @@ -202,15 +202,15 @@
     1.4  
     1.5      val atoms = atoms_of thy;
     1.6  
     1.7 -    fun prep_constr ((constrs, sorts), (cname, cargs, mx)) =
     1.8 -      let val (cargs', sorts') = Library.foldl (prep_typ tmp_thy) (([], sorts), cargs)
     1.9 +    fun prep_constr (cname, cargs, mx) (constrs, sorts) =
    1.10 +      let val (cargs', sorts') = fold_map (prep_typ tmp_thy) cargs sorts
    1.11        in (constrs @ [(cname, cargs', mx)], sorts') end
    1.12  
    1.13 -    fun prep_dt_spec ((dts, sorts), (tvs, tname, mx, constrs)) =
    1.14 -      let val (constrs', sorts') = Library.foldl prep_constr (([], sorts), constrs)
    1.15 +    fun prep_dt_spec (tvs, tname, mx, constrs) (dts, sorts) =
    1.16 +      let val (constrs', sorts') = fold prep_constr constrs ([], sorts)
    1.17        in (dts @ [(tvs, tname, mx, constrs')], sorts') end
    1.18  
    1.19 -    val (dts', sorts) = Library.foldl prep_dt_spec (([], []), dts);
    1.20 +    val (dts', sorts) = fold prep_dt_spec dts ([], []);
    1.21      val tyvars = map (map (fn s =>
    1.22        (s, the (AList.lookup (op =) sorts s))) o #1) dts';
    1.23  
    1.24 @@ -770,8 +770,8 @@
    1.25  
    1.26      val full_new_type_names = map (Sign.full_bname thy) new_type_names;
    1.27  
    1.28 -    fun make_constr_def tname T T' ((thy, defs, eqns),
    1.29 -        (((cname_rep, _), (cname, cargs)), (cname', mx))) =
    1.30 +    fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
    1.31 +        (thy, defs, eqns) =
    1.32        let
    1.33          fun constr_arg ((dts, dt), (j, l_args, r_args)) =
    1.34            let
    1.35 @@ -805,22 +805,24 @@
    1.36            (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
    1.37        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
    1.38  
    1.39 -    fun dt_constr_defs ((thy, defs, eqns, dist_lemmas), ((((((_, (_, _, constrs)),
    1.40 -        (_, (_, _, constrs'))), tname), T), T'), constr_syntax)) =
    1.41 +    fun dt_constr_defs ((((((_, (_, _, constrs)),
    1.42 +        (_, (_, _, constrs'))), tname), T), T'), constr_syntax) (thy, defs, eqns, dist_lemmas) =
    1.43        let
    1.44          val rep_const = cterm_of thy
    1.45            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
    1.46 -        val dist = Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    1.47 -        val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
    1.48 -          ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
    1.49 +        val dist =
    1.50 +          Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    1.51 +        val (thy', defs', eqns') = fold (make_constr_def tname T T')
    1.52 +          (constrs ~~ constrs' ~~ constr_syntax) (Sign.add_path tname thy, defs, [])
    1.53        in
    1.54          (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
    1.55        end;
    1.56  
    1.57 -    val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs
    1.58 -      ((thy7, [], [], []), List.take (descr, length new_type_names) ~~
    1.59 +    val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = fold dt_constr_defs
    1.60 +      (List.take (descr, length new_type_names) ~~
    1.61          List.take (pdescr, length new_type_names) ~~
    1.62 -        new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax);
    1.63 +        new_type_names ~~ newTs ~~ newTs' ~~ constr_syntax)
    1.64 +      (thy7, [], [], []);
    1.65  
    1.66      val abs_inject_thms = map (collect_simp o #Abs_inject o fst) typedefs
    1.67      val rep_inject_thms = map (#Rep_inject o fst) typedefs
    1.68 @@ -1031,7 +1033,7 @@
    1.69  
    1.70      (**** weak induction theorem ****)
    1.71  
    1.72 -    fun mk_indrule_lemma ((prems, concls), (((i, _), T), U)) =
    1.73 +    fun mk_indrule_lemma (((i, _), T), U) (prems, concls) =
    1.74        let
    1.75          val Rep_t = Const (List.nth (rep_names, i), T --> U) $
    1.76            mk_Free "x" T i;
    1.77 @@ -1045,7 +1047,7 @@
    1.78        end;
    1.79  
    1.80      val (indrule_lemma_prems, indrule_lemma_concls) =
    1.81 -      Library.foldl mk_indrule_lemma (([], []), (descr'' ~~ recTs ~~ recTs'));
    1.82 +      fold mk_indrule_lemma (descr'' ~~ recTs ~~ recTs') ([], []);
    1.83  
    1.84      val indrule_lemma = Goal.prove_global thy8 [] []
    1.85        (Logic.mk_implies
    1.86 @@ -1455,8 +1457,8 @@
    1.87      (* FIXME: avoid collisions with other variable names? *)
    1.88      val rec_ctxt = Free ("z", fsT');
    1.89  
    1.90 -    fun make_rec_intr T p rec_set ((rec_intr_ts, rec_prems, rec_prems',
    1.91 -          rec_eq_prems, l), ((cname, cargs), idxs)) =
    1.92 +    fun make_rec_intr T p rec_set ((cname, cargs), idxs)
    1.93 +        (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) =
    1.94        let
    1.95          val Ts = map (typ_of_dtyp descr'' sorts) cargs;
    1.96          val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts;
    1.97 @@ -1500,9 +1502,10 @@
    1.98        end;
    1.99  
   1.100      val (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, _) =
   1.101 -      Library.foldl (fn (x, ((((d, d'), T), p), rec_set)) =>
   1.102 -        Library.foldl (make_rec_intr T p rec_set) (x, #3 (snd d) ~~ snd d'))
   1.103 -          (([], [], [], [], 0), descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets');
   1.104 +      fold (fn ((((d, d'), T), p), rec_set) =>
   1.105 +        fold (make_rec_intr T p rec_set) (#3 (snd d) ~~ snd d'))
   1.106 +          (descr'' ~~ ndescr ~~ recTs ~~ rec_preds ~~ rec_sets')
   1.107 +          ([], [], [], [], 0);
   1.108  
   1.109      val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
   1.110        thy10 |>
     2.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Tue Oct 27 17:34:00 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Tue Oct 27 22:55:27 2009 +0100
     2.3 @@ -301,9 +301,9 @@
     2.4              val ps = Logic.strip_params (term_of goal);
     2.5              val Ts = rev (map snd ps);
     2.6              val vs = collect_vars 0 x [];
     2.7 -            val s = Library.foldr (fn (v, s) =>
     2.8 +            val s = fold_rev (fn v => fn s =>
     2.9                  HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
    2.10 -              (vs, HOLogic.unit);
    2.11 +              vs HOLogic.unit;
    2.12              val s' = list_abs (ps,
    2.13                Const ("Nominal.supp", fastype_of1 (Ts, s) -->
    2.14                  snd (split_last (binder_types T)) --> HOLogic.boolT) $ s);
    2.15 @@ -343,9 +343,9 @@
    2.16              val ps = Logic.strip_params (term_of goal);
    2.17              val Ts = rev (map snd ps);
    2.18              val vs = collect_vars 0 t [];
    2.19 -            val s = Library.foldr (fn (v, s) =>
    2.20 +            val s = fold_rev (fn v => fn s =>
    2.21                  HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
    2.22 -              (vs, HOLogic.unit);
    2.23 +              vs HOLogic.unit;
    2.24              val s' = list_abs (ps,
    2.25                Const ("Nominal.supp", fastype_of1 (Ts, s) --> (HOLogic.mk_setT T)) $ s);
    2.26              val supports_fresh_rule' = Thm.lift_rule goal supports_fresh_rule;
     3.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 27 17:34:00 2009 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 27 22:55:27 2009 +0100
     3.3 @@ -29,8 +29,7 @@
     3.4    val make_case :  Proof.context -> DatatypeCase.config -> string list -> term ->
     3.5      (term * term) list -> term * (term * (int * bool)) list
     3.6    val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
     3.7 -  val read_typ: theory ->
     3.8 -    (typ list * (string * sort) list) * string -> typ list * (string * sort) list
     3.9 +  val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list
    3.10    val setup: theory -> theory
    3.11  end;
    3.12  
    3.13 @@ -160,23 +159,24 @@
    3.14  
    3.15  (* prepare datatype specifications *)
    3.16  
    3.17 -fun read_typ thy ((Ts, sorts), str) =
    3.18 +fun read_typ thy str sorts =
    3.19    let
    3.20      val ctxt = ProofContext.init thy
    3.21        |> fold (Variable.declare_typ o TFree) sorts;
    3.22      val T = Syntax.read_typ ctxt str;
    3.23 -  in (Ts @ [T], Term.add_tfreesT T sorts) end;
    3.24 +  in (T, Term.add_tfreesT T sorts) end;
    3.25  
    3.26 -fun cert_typ sign ((Ts, sorts), raw_T) =
    3.27 +fun cert_typ sign raw_T sorts =
    3.28    let
    3.29 -    val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
    3.30 -      TYPE (msg, _, _) => error msg;
    3.31 +    val T = Type.no_tvars (Sign.certify_typ sign raw_T)
    3.32 +      handle TYPE (msg, _, _) => error msg;
    3.33      val sorts' = Term.add_tfreesT T sorts;
    3.34 -  in (Ts @ [T],
    3.35 +    val _ =
    3.36        case duplicates (op =) (map fst sorts') of
    3.37 -         [] => sorts'
    3.38 -       | dups => error ("Inconsistent sort constraints for " ^ commas dups))
    3.39 -  end;
    3.40 +        [] => ()
    3.41 +      | dups => error ("Inconsistent sort constraints for " ^ commas dups)
    3.42 +  in (T, sorts') end;
    3.43 +
    3.44  
    3.45  (* case names *)
    3.46  
    3.47 @@ -460,8 +460,9 @@
    3.48        let
    3.49          fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
    3.50            let
    3.51 -            val (cargs', sorts'') = Library.foldl (prep_typ tmp_thy) (([], sorts'), cargs);
    3.52 -            val _ = (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
    3.53 +            val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
    3.54 +            val _ =
    3.55 +              (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
    3.56                  [] => ()
    3.57                | vs => error ("Extra type variables on rhs: " ^ commas vs))
    3.58            in (constrs @ [(Sign.full_name_path tmp_thy tname'
     4.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 17:34:00 2009 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 22:55:27 2009 +0100
     4.3 @@ -255,9 +255,8 @@
     4.4  (* find all non-recursive types in datatype description *)
     4.5  
     4.6  fun get_nonrec_types descr sorts =
     4.7 -  map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
     4.8 -    Library.foldl (fn (Ts', (_, cargs)) =>
     4.9 -      union (op =) (filter_out is_rec_type cargs) Ts') (Ts, constrs)) ([], descr));
    4.10 +  map (typ_of_dtyp descr sorts) (fold (fn (_, (_, _, constrs)) =>
    4.11 +    fold (fn (_, cargs) => union (op =) (filter_out is_rec_type cargs)) constrs) descr []);
    4.12  
    4.13  (* get all recursive types in datatype description *)
    4.14  
    4.15 @@ -335,7 +334,7 @@
    4.16  
    4.17      (* unfold a single constructor argument *)
    4.18  
    4.19 -    fun unfold_arg ((i, Ts, descrs), T) =
    4.20 +    fun unfold_arg T (i, Ts, descrs) =
    4.21        if is_rec_type T then
    4.22          let val (Us, U) = strip_dtyp T
    4.23          in if exists is_rec_type Us then
    4.24 @@ -353,19 +352,17 @@
    4.25  
    4.26      (* unfold a constructor *)
    4.27  
    4.28 -    fun unfold_constr ((i, constrs, descrs), (cname, cargs)) =
    4.29 -      let val (i', cargs', descrs') = Library.foldl unfold_arg ((i, [], descrs), cargs)
    4.30 +    fun unfold_constr (cname, cargs) (i, constrs, descrs) =
    4.31 +      let val (i', cargs', descrs') = fold unfold_arg cargs (i, [], descrs)
    4.32        in (i', constrs @ [(cname, cargs')], descrs') end;
    4.33  
    4.34      (* unfold a single datatype *)
    4.35  
    4.36 -    fun unfold_datatype ((i, dtypes, descrs), (j, (tname, tvars, constrs))) =
    4.37 -      let val (i', constrs', descrs') =
    4.38 -        Library.foldl unfold_constr ((i, [], descrs), constrs)
    4.39 -      in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs')
    4.40 -      end;
    4.41 +    fun unfold_datatype (j, (tname, tvars, constrs)) (i, dtypes, descrs) =
    4.42 +      let val (i', constrs', descrs') = fold unfold_constr constrs (i, [], descrs)
    4.43 +      in (i', dtypes @ [(j, (tname, tvars, constrs'))], descrs') end;
    4.44  
    4.45 -    val (i', descr', descrs) = Library.foldl unfold_datatype ((i, [],[]), descr);
    4.46 +    val (i', descr', descrs) = fold unfold_datatype descr (i, [], []);
    4.47  
    4.48    in (descr' :: descrs, i') end;
    4.49  
     5.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Oct 27 17:34:00 2009 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Oct 27 22:55:27 2009 +0100
     5.3 @@ -221,7 +221,7 @@
     5.4        (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
     5.5          (reccomb_names ~~ recTs ~~ rec_result_Ts);
     5.6  
     5.7 -    fun make_primrec T comb_t ((ts, f::fs), (cname, cargs)) =
     5.8 +    fun make_primrec T comb_t (cname, cargs) (ts, f::fs) =
     5.9        let
    5.10          val recs = List.filter is_rec_type cargs;
    5.11          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    5.12 @@ -242,11 +242,12 @@
    5.13        in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
    5.14          (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
    5.15           list_comb (f, frees @ reccombs')))], fs)
    5.16 -      end
    5.17 +      end;
    5.18  
    5.19 -  in fst (Library.foldl (fn (x, ((dt, T), comb_t)) =>
    5.20 -    Library.foldl (make_primrec T comb_t) (x, #3 (snd dt)))
    5.21 -      (([], rec_fns), descr' ~~ recTs ~~ reccombs))
    5.22 +  in
    5.23 +    fold (fn ((dt, T), comb_t) => fold (make_primrec T comb_t) (#3 (snd dt)))
    5.24 +      (descr' ~~ recTs ~~ reccombs) ([], rec_fns)
    5.25 +    |> fst
    5.26    end;
    5.27  
    5.28  (****************** make terms of form  t_case f1 ... fn  *********************)
     6.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Oct 27 17:34:00 2009 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Oct 27 22:55:27 2009 +0100
     6.3 @@ -207,7 +207,7 @@
     6.4  
     6.5      (* constructor definitions *)
     6.6  
     6.7 -    fun make_constr_def tname T n ((thy, defs, eqns, i), ((cname, cargs), (cname', mx))) =
     6.8 +    fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
     6.9        let
    6.10          fun constr_arg (dt, (j, l_args, r_args)) =
    6.11            let val T = typ_of_dtyp descr' sorts dt;
    6.12 @@ -238,8 +238,8 @@
    6.13  
    6.14      (* constructor definitions for datatype *)
    6.15  
    6.16 -    fun dt_constr_defs ((thy, defs, eqns, rep_congs, dist_lemmas),
    6.17 -        ((((_, (_, _, constrs)), tname), T), constr_syntax)) =
    6.18 +    fun dt_constr_defs ((((_, (_, _, constrs)), tname), T), constr_syntax)
    6.19 +        (thy, defs, eqns, rep_congs, dist_lemmas) =
    6.20        let
    6.21          val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
    6.22          val rep_const = cterm_of thy
    6.23 @@ -248,16 +248,18 @@
    6.24            Drule.standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
    6.25          val dist =
    6.26            Drule.standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    6.27 -        val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
    6.28 -          ((Sign.add_path tname thy, defs, [], 1), constrs ~~ constr_syntax)
    6.29 +        val (thy', defs', eqns', _) = fold ((make_constr_def tname T) (length constrs))
    6.30 +          (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1);
    6.31        in
    6.32          (Sign.parent_path thy', defs', eqns @ [eqns'],
    6.33            rep_congs @ [cong'], dist_lemmas @ [dist])
    6.34        end;
    6.35  
    6.36 -    val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
    6.37 -      ((thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []),
    6.38 -        hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
    6.39 +    val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) =
    6.40 +      fold dt_constr_defs
    6.41 +        (hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax)
    6.42 +        (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []);
    6.43 +
    6.44  
    6.45      (*********** isomorphisms for new types (introduced by typedef) ***********)
    6.46  
    6.47 @@ -283,7 +285,7 @@
    6.48      (*   e.g.  dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *)
    6.49      (*---------------------------------------------------------------------*)
    6.50  
    6.51 -    fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
    6.52 +    fun make_iso_def k ks n (cname, cargs) (fs, eqns, i) =
    6.53        let
    6.54          val argTs = map (typ_of_dtyp descr' sorts) cargs;
    6.55          val T = nth recTs k;
    6.56 @@ -291,7 +293,7 @@
    6.57          val rep_const = Const (rep_name, T --> Univ_elT);
    6.58          val constr = Const (cname, argTs ---> T);
    6.59  
    6.60 -        fun process_arg ks' ((i2, i2', ts, Ts), dt) =
    6.61 +        fun process_arg ks' dt (i2, i2', ts, Ts) =
    6.62            let
    6.63              val T' = typ_of_dtyp descr' sorts dt;
    6.64              val (Us, U) = strip_type T'
    6.65 @@ -307,12 +309,12 @@
    6.66              | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
    6.67            end;
    6.68  
    6.69 -        val (i2, i2', ts, Ts) = Library.foldl (process_arg ks) ((1, 1, [], []), cargs);
    6.70 +        val (i2, i2', ts, Ts) = fold (process_arg ks) cargs (1, 1, [], []);
    6.71          val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1)));
    6.72          val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1)));
    6.73          val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i);
    6.74  
    6.75 -        val (_, _, ts', _) = Library.foldl (process_arg []) ((1, 1, [], []), cargs);
    6.76 +        val (_, _, ts', _) = fold (process_arg []) cargs (1, 1, [], []);
    6.77          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    6.78            (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i))
    6.79  
    6.80 @@ -320,20 +322,20 @@
    6.81  
    6.82      (* define isomorphisms for all mutually recursive datatypes in list ds *)
    6.83  
    6.84 -    fun make_iso_defs (ds, (thy, char_thms)) =
    6.85 +    fun make_iso_defs ds (thy, char_thms) =
    6.86        let
    6.87          val ks = map fst ds;
    6.88          val (_, (tname, _, _)) = hd ds;
    6.89          val {rec_rewrites, rec_names, ...} = the (Symtab.lookup dt_info tname);
    6.90  
    6.91 -        fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) =
    6.92 +        fun process_dt (k, (tname, _, constrs)) (fs, eqns, isos) =
    6.93            let
    6.94 -            val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs))
    6.95 -              ((fs, eqns, 1), constrs);
    6.96 +            val (fs', eqns', _) =
    6.97 +              fold (make_iso_def k ks (length constrs)) constrs (fs, eqns, 1);
    6.98              val iso = (nth recTs k, nth all_rep_names k)
    6.99            in (fs', eqns', isos @ [iso]) end;
   6.100          
   6.101 -        val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
   6.102 +        val (fs, eqns, isos) = fold process_dt ds ([], [], []);
   6.103          val fTs = map fastype_of fs;
   6.104          val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"),
   6.105            Logic.mk_equals (Const (iso_name, T --> Univ_elT),
   6.106 @@ -349,8 +351,8 @@
   6.107  
   6.108        in (thy', char_thms' @ char_thms) end;
   6.109  
   6.110 -    val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
   6.111 -      (Sign.add_path big_name thy4, []) (tl descr));
   6.112 +    val (thy5, iso_char_thms) = apfst Theory.checkpoint (fold_rev make_iso_defs
   6.113 +        (tl descr) (Sign.add_path big_name thy4, []));
   6.114  
   6.115      (* prove isomorphism properties *)
   6.116  
   6.117 @@ -563,7 +565,7 @@
   6.118        (map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded);
   6.119      val Rep_inverse_thms' = map (fn r => r RS @{thm the_inv_f_f}) iso_inj_thms_unfolded;
   6.120  
   6.121 -    fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
   6.122 +    fun mk_indrule_lemma ((i, _), T) (prems, concls) =
   6.123        let
   6.124          val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $
   6.125            mk_Free "x" T i;
   6.126 @@ -582,7 +584,7 @@
   6.127        end;
   6.128  
   6.129      val (indrule_lemma_prems, indrule_lemma_concls) =
   6.130 -      Library.foldl mk_indrule_lemma (([], []), (descr' ~~ recTs));
   6.131 +      fold mk_indrule_lemma (descr' ~~ recTs) ([], []);
   6.132  
   6.133      val cert = cterm_of thy6;
   6.134  
     7.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Oct 27 17:34:00 2009 +0100
     7.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Oct 27 22:55:27 2009 +0100
     7.3 @@ -41,7 +41,7 @@
     7.4  fun warn thm = warning ("InductiveCodegen: Not a proper clause:\n" ^
     7.5    Display.string_of_thm_without_context thm);
     7.6  
     7.7 -fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
     7.8 +fun add_node x g = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
     7.9  
    7.10  fun add optmod optnparms = Thm.declaration_attribute (fn thm => Context.mapping (fn thy =>
    7.11    let
    7.12 @@ -72,7 +72,7 @@
    7.13             Symtab.update (s, (AList.update Thm.eq_thm_prop
    7.14               (thm, (thyname_of s, nparms)) rules)),
    7.15             graph = List.foldr (uncurry (Graph.add_edge o pair s))
    7.16 -             (Library.foldl add_node (graph, s :: cs)) cs,
    7.17 +             (fold add_node (s :: cs) graph) cs,
    7.18             eqns = eqns} thy
    7.19          end
    7.20      | _ => (warn thm; thy))
    7.21 @@ -266,19 +266,22 @@
    7.22    flat (separate [str ",", Pretty.brk 1] (map single xs)) @
    7.23    [str ")"]);
    7.24  
    7.25 -fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
    7.26 -      NONE => ((names, (s, [s])::vs), s)
    7.27 -    | SOME xs => let val s' = Name.variant names s in
    7.28 -        ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
    7.29 +fun mk_v s (names, vs) =
    7.30 +  (case AList.lookup (op =) vs s of
    7.31 +    NONE => (s, (names, (s, [s])::vs))
    7.32 +  | SOME xs =>
    7.33 +      let val s' = Name.variant names s
    7.34 +      in (s', (s'::names, AList.update (op =) (s, s'::xs) vs)) end);
    7.35  
    7.36 -fun distinct_v (nvs, Var ((s, 0), T)) =
    7.37 -      apsnd (Var o rpair T o rpair 0) (mk_v (nvs, s))
    7.38 -  | distinct_v (nvs, t $ u) =
    7.39 +fun distinct_v (Var ((s, 0), T)) nvs =
    7.40 +      let val (s', nvs') = mk_v s nvs
    7.41 +      in (Var ((s', 0), T), nvs') end
    7.42 +  | distinct_v (t $ u) nvs =
    7.43        let
    7.44 -        val (nvs', t') = distinct_v (nvs, t);
    7.45 -        val (nvs'', u') = distinct_v (nvs', u);
    7.46 -      in (nvs'', t' $ u') end
    7.47 -  | distinct_v x = x;
    7.48 +        val (t', nvs') = distinct_v t nvs;
    7.49 +        val (u', nvs'') = distinct_v u nvs';
    7.50 +      in (t' $ u', nvs'') end
    7.51 +  | distinct_v t nvs = (t, nvs);
    7.52  
    7.53  fun is_exhaustive (Var _) = true
    7.54    | is_exhaustive (Const ("Pair", _) $ t $ u) =
    7.55 @@ -346,30 +349,29 @@
    7.56        (fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
    7.57          (arg_vs ~~ iss);
    7.58  
    7.59 -    fun check_constrt ((names, eqs), t) =
    7.60 -      if is_constrt thy t then ((names, eqs), t) else
    7.61 +    fun check_constrt t (names, eqs) =
    7.62 +      if is_constrt thy t then (t, (names, eqs))
    7.63 +      else
    7.64          let val s = Name.variant names "x";
    7.65 -        in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
    7.66 +        in (Var ((s, 0), fastype_of t), (s::names, (s, t)::eqs)) end;
    7.67  
    7.68      fun compile_eq (s, t) gr =
    7.69        apfst (Pretty.block o cons (str (s ^ " = ")) o single)
    7.70          (invoke_codegen thy defs dep module false t gr);
    7.71  
    7.72      val (in_ts, out_ts) = get_args is 1 ts;
    7.73 -    val ((all_vs', eqs), in_ts') =
    7.74 -      Library.foldl_map check_constrt ((all_vs, []), in_ts);
    7.75 +    val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []);
    7.76  
    7.77      fun compile_prems out_ts' vs names [] gr =
    7.78            let
    7.79 -            val (out_ps, gr2) = fold_map
    7.80 -              (invoke_codegen thy defs dep module false) out_ts gr;
    7.81 +            val (out_ps, gr2) =
    7.82 +              fold_map (invoke_codegen thy defs dep module false) out_ts gr;
    7.83              val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
    7.84 -            val ((names', eqs'), out_ts'') =
    7.85 -              Library.foldl_map check_constrt ((names, []), out_ts');
    7.86 -            val (nvs, out_ts''') = Library.foldl_map distinct_v
    7.87 -              ((names', map (fn x => (x, [x])) vs), out_ts'');
    7.88 -            val (out_ps', gr4) = fold_map
    7.89 -              (invoke_codegen thy defs dep module false) (out_ts''') gr3;
    7.90 +            val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []);
    7.91 +            val (out_ts''', nvs) =
    7.92 +              fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs);
    7.93 +            val (out_ps', gr4) =
    7.94 +              fold_map (invoke_codegen thy defs dep module false) out_ts''' gr3;
    7.95              val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
    7.96            in
    7.97              (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
    7.98 @@ -379,15 +381,11 @@
    7.99        | compile_prems out_ts vs names ps gr =
   7.100            let
   7.101              val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
   7.102 -            val SOME (p, mode as SOME (Mode (_, js, _))) =
   7.103 -              select_mode_prem thy modes' vs' ps;
   7.104 +            val SOME (p, mode as SOME (Mode (_, js, _))) = select_mode_prem thy modes' vs' ps;
   7.105              val ps' = filter_out (equal p) ps;
   7.106 -            val ((names', eqs), out_ts') =
   7.107 -              Library.foldl_map check_constrt ((names, []), out_ts);
   7.108 -            val (nvs, out_ts'') = Library.foldl_map distinct_v
   7.109 -              ((names', map (fn x => (x, [x])) vs), out_ts');
   7.110 -            val (out_ps, gr0) = fold_map
   7.111 -              (invoke_codegen thy defs dep module false) out_ts'' gr;
   7.112 +            val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []);
   7.113 +            val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs);
   7.114 +            val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr;
   7.115              val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
   7.116            in
   7.117              (case p of
   7.118 @@ -480,19 +478,22 @@
   7.119  fun prep_intrs intrs = map (rename_term o #prop o rep_thm o Drule.standard) intrs;
   7.120  
   7.121  fun constrain cs [] = []
   7.122 -  | constrain cs ((s, xs) :: ys) = (s, case AList.lookup (op =) cs (s : string) of
   7.123 -      NONE => xs
   7.124 -    | SOME xs' => inter (op =) xs' xs) :: constrain cs ys;
   7.125 +  | constrain cs ((s, xs) :: ys) =
   7.126 +      (s,
   7.127 +        case AList.lookup (op =) cs (s : string) of
   7.128 +          NONE => xs
   7.129 +        | SOME xs' => inter (op =) xs' xs) :: constrain cs ys;
   7.130  
   7.131  fun mk_extra_defs thy defs gr dep names module ts =
   7.132 -  Library.foldl (fn (gr, name) =>
   7.133 +  fold (fn name => fn gr =>
   7.134      if name mem names then gr
   7.135 -    else (case get_clauses thy name of
   7.136 +    else
   7.137 +      (case get_clauses thy name of
   7.138          NONE => gr
   7.139        | SOME (names, thyname, nparms, intrs) =>
   7.140            mk_ind_def thy defs gr dep names (if_library thyname module)
   7.141              [] (prep_intrs intrs) nparms))
   7.142 -            (gr, fold Term.add_const_names ts [])
   7.143 +    (fold Term.add_const_names ts []) gr
   7.144  
   7.145  and mk_ind_def thy defs gr dep names module modecs intrs nparms =
   7.146    add_edge_acyclic (hd names, dep) gr handle
   7.147 @@ -562,17 +563,16 @@
   7.148      val (ts1, ts2) = chop k ts;
   7.149      val u = list_comb (Const (s, T), ts1);
   7.150  
   7.151 -    fun mk_mode (((ts, mode), i), Const ("dummy_pattern", _)) =
   7.152 -          ((ts, mode), i+1)
   7.153 -      | mk_mode (((ts, mode), i), t) = ((ts @ [t], mode @ [i]), i+1);
   7.154 +    fun mk_mode (Const ("dummy_pattern", _)) ((ts, mode), i) = ((ts, mode), i + 1)
   7.155 +      | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1);
   7.156  
   7.157      val module' = if_library thyname module;
   7.158      val gr1 = mk_extra_defs thy defs
   7.159        (mk_ind_def thy defs gr dep names module'
   7.160        [] (prep_intrs intrs) k) dep names module' [u];
   7.161      val (modes, _) = lookup_modes gr1 dep;
   7.162 -    val (ts', is) = if is_query then
   7.163 -        fst (Library.foldl mk_mode ((([], []), 1), ts2))
   7.164 +    val (ts', is) =
   7.165 +      if is_query then fst (fold mk_mode ts2 (([], []), 1))
   7.166        else (ts2, 1 upto length (binder_types T) - k);
   7.167      val mode = find_mode gr1 dep s u modes is;
   7.168      val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1;
   7.169 @@ -697,8 +697,9 @@
   7.170  
   7.171  val setup =
   7.172    add_codegen "inductive" inductive_codegen #>
   7.173 -  Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
   7.174 -    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
   7.175 +  Attrib.setup @{binding code_ind}
   7.176 +    (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
   7.177 +      Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
   7.178      "introduction rules for executable predicates";
   7.179  
   7.180  end;
     8.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Oct 27 17:34:00 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Oct 27 22:55:27 2009 +0100
     8.3 @@ -271,7 +271,7 @@
     8.4  
     8.5  fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
     8.6  
     8.7 -fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
     8.8 +fun add_ind_realizer rsets intrs induct raw_induct elims vs thy =
     8.9    let
    8.10      val qualifier = Long_Name.qualifier (name_of_thm induct);
    8.11      val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
    8.12 @@ -367,7 +367,7 @@
    8.13        SOME (fst (fst (dest_Var (head_of P)))) else NONE)
    8.14          (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
    8.15  
    8.16 -    fun add_ind_realizer (thy, Ps) =
    8.17 +    fun add_ind_realizer Ps thy =
    8.18        let
    8.19          val vs' = rename (map (pairself (fst o fst o dest_Var))
    8.20            (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
    8.21 @@ -426,13 +426,12 @@
    8.22        let
    8.23          val (prem :: prems) = prems_of elim;
    8.24          fun reorder1 (p, (_, intr)) =
    8.25 -          Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t)
    8.26 -            (strip_all p, subtract (op =) params' (Term.add_vars (prop_of intr) []));
    8.27 +          fold (fn ((s, _), T) => Logic.all (Free (s, T)))
    8.28 +            (subtract (op =) params' (Term.add_vars (prop_of intr) []))
    8.29 +            (strip_all p);
    8.30          fun reorder2 ((ivs, intr), i) =
    8.31            let val fs = subtract (op =) params' (Term.add_vars (prop_of intr) [])
    8.32 -          in Library.foldl (fn (t, x) => lambda (Var x) t)
    8.33 -            (list_comb (Bound (i + length ivs), ivs), fs)
    8.34 -          end;
    8.35 +          in fold (lambda o Var) fs (list_comb (Bound (i + length ivs), ivs)) end;
    8.36          val p = Logic.list_implies
    8.37            (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim);
    8.38          val T' = Extraction.etype_of thy (vs @ Ps) [] p;
    8.39 @@ -465,7 +464,7 @@
    8.40  
    8.41      (** add realizers to theory **)
    8.42  
    8.43 -    val thy4 = Library.foldl add_ind_realizer (thy3, subsets Ps);
    8.44 +    val thy4 = fold add_ind_realizer (subsets Ps) thy3;
    8.45      val thy5 = Extraction.add_realizers_i
    8.46        (map (mk_realizer thy4 vs) (map (fn (((rule, rrule), rlz), c) =>
    8.47           (name_of_thm rule, rule, rrule, rlz,
    8.48 @@ -474,10 +473,11 @@
    8.49      val elimps = map_filter (fn ((s, intrs), p) =>
    8.50        if s mem rsets then SOME (p, intrs) else NONE)
    8.51          (rss' ~~ (elims ~~ #elims ind_info));
    8.52 -    val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |>
    8.53 -      add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var
    8.54 -        (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
    8.55 -           elimps ~~ case_thms ~~ case_names ~~ dummies)
    8.56 +    val thy6 =
    8.57 +      fold (fn p as (((((elim, _), _), _), _), _) =>
    8.58 +        add_elim_realizer [] p #>
    8.59 +        add_elim_realizer [fst (fst (dest_Var (HOLogic.dest_Trueprop (concl_of elim))))] p)
    8.60 +      (elimps ~~ case_thms ~~ case_names ~~ dummies) thy5;
    8.61  
    8.62    in Sign.restore_naming thy thy6 end;
    8.63  
    8.64 @@ -488,7 +488,7 @@
    8.65      val vss = sort (int_ord o pairself length)
    8.66        (subsets (map fst (relevant_vars (concl_of (hd intrs)))))
    8.67    in
    8.68 -    Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
    8.69 +    fold (add_ind_realizer rsets intrs induct raw_induct elims) vss thy
    8.70    end
    8.71  
    8.72  fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
     9.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Oct 27 17:34:00 2009 +0100
     9.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Oct 27 22:55:27 2009 +0100
     9.3 @@ -65,9 +65,9 @@
     9.4  
     9.5  exception EQN of string * typ * string;
     9.6  
     9.7 -fun cycle g (xs, x : string) =
     9.8 +fun cycle g x xs =
     9.9    if member (op =) xs x then xs
    9.10 -  else Library.foldl (cycle g) (x :: xs, flat (Graph.all_paths (fst g) (x, x)));
    9.11 +  else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
    9.12  
    9.13  fun add_rec_funs thy defs dep module eqs gr =
    9.14    let
    9.15 @@ -107,7 +107,7 @@
    9.16             val gr1 = add_edge (dname, dep)
    9.17               (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr);
    9.18             val (fundef, gr2) = mk_fundef module "" true eqs' gr1 ;
    9.19 -           val xs = cycle gr2 ([], dname);
    9.20 +           val xs = cycle gr2 dname [];
    9.21             val cs = map (fn x => case get_node gr2 x of
    9.22                 (SOME (EQN (s, T, _)), _, _) => (s, T)
    9.23               | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^