--- a/src/FOLP/simp.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/FOLP/simp.ML Thu Oct 29 23:58:15 2009 +0100
@@ -66,7 +66,7 @@
fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Thm.eq_thm_prop (th1, th2);
(*insert a thm in a discrimination net by its lhs*)
-fun lhs_insert_thm (th,net) =
+fun lhs_insert_thm th net =
Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net
handle Net.INSERT => net;
@@ -434,7 +434,7 @@
val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
val new_rws = maps mk_rew_rules thms;
val rwrls = map mk_trans (maps mk_rew_rules thms);
- val anet' = List.foldr lhs_insert_thm anet rwrls
+ val anet' = fold_rev lhs_insert_thm rwrls anet;
in if !tracing andalso not(null new_rws)
then writeln (cat_lines
("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
--- a/src/HOL/Import/lazy_seq.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Import/lazy_seq.ML Thu Oct 29 23:58:15 2009 +0100
@@ -407,8 +407,8 @@
make (fn () => copy (f x))
end
-fun EVERY fs = List.foldr (op THEN) succeed fs
-fun FIRST fs = List.foldr (op ORELSE) fail fs
+fun EVERY fs = fold_rev (curry op THEN) fs succeed
+fun FIRST fs = fold_rev (curry op ORELSE) fs fail
fun TRY f x =
make (fn () =>
--- a/src/HOL/Import/proof_kernel.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Import/proof_kernel.ML Thu Oct 29 23:58:15 2009 +0100
@@ -776,7 +776,7 @@
val (c,asl) = case terms of
[] => raise ERR "x2p" "Bad oracle description"
| (hd::tl) => (hd,tl)
- val tg = List.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
+ val tg = fold_rev (Tag.merge o Tag.read) ors Tag.empty_tag
in
mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
end
@@ -1160,7 +1160,7 @@
| replace_name n' _ = ERR "replace_name"
(* map: old or fresh name -> old free,
invmap: old free which has fresh name assigned to it -> fresh name *)
- fun dis (v, mapping as (map,invmap)) =
+ fun dis v (mapping as (map,invmap)) =
let val n = name_of v in
case Symtab.lookup map n of
NONE => (Symtab.update (n, v) map, invmap)
@@ -1179,11 +1179,11 @@
else
let
val (_, invmap) =
- List.foldl dis (Symtab.empty, Termtab.empty) frees
- fun make_subst ((oldfree, newname), (intros, elims)) =
+ fold dis frees (Symtab.empty, Termtab.empty)
+ fun make_subst (oldfree, newname) (intros, elims) =
(cterm_of thy oldfree :: intros,
cterm_of thy (replace_name newname oldfree) :: elims)
- val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap)
+ val (intros, elims) = fold make_subst (Termtab.dest invmap) ([], [])
in
forall_elim_list elims (forall_intr_list intros thm)
end
@@ -1837,7 +1837,7 @@
| inst_type ty1 ty2 (ty as Type(name,tys)) =
Type(name,map (inst_type ty1 ty2) tys)
in
- List.foldr (fn (v,th) =>
+ fold_rev (fn v => fn th =>
let
val cdom = fst (dom_rng (fst (dom_rng cty)))
val vty = type_of v
@@ -1845,11 +1845,11 @@
val cc = cterm_of thy (Const(cname,newcty))
in
mk_COMB (mk_REFL cc) (mk_ABS v th thy) thy
- end) th vlist'
+ end) vlist' th
end
| SOME _ => raise ERR "GEN_ABS" "Bad constant"
| NONE =>
- List.foldr (fn (v,th) => mk_ABS v th thy) th vlist'
+ fold_rev (fn v => fn th => mk_ABS v th thy) vlist' th
val res = HOLThm(rens_of info',th1)
val _ = message "RESULT:"
val _ = if_debug pth res
@@ -2020,8 +2020,8 @@
Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
end
- val thy1 = List.foldr (fn(name,thy)=>
- snd (get_defname thyname name thy)) thy1 names
+ val thy1 = fold_rev (fn name => fn thy =>
+ snd (get_defname thyname name thy)) names thy1
fun new_name name = fst (get_defname thyname name thy1)
val names' = map (fn name => (new_name name,name,false)) names
val (thy',res) = Choice_Specification.add_specification NONE
@@ -2041,12 +2041,12 @@
then quotename name
else (quotename newname) ^ ": " ^ (quotename name),thy')
end
- val (new_names,thy') = List.foldr (fn(name,(names,thy)) =>
+ val (new_names,thy') = fold_rev (fn name => fn (names, thy) =>
let
val (name',thy') = handle_const (name,thy)
in
(name'::names,thy')
- end) ([],thy') names
+ end) names ([], thy')
val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
"\n by (import " ^ thyname ^ " " ^ thmname ^ ")")
thy'
--- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Thu Oct 29 23:58:15 2009 +0100
@@ -100,7 +100,7 @@
(fn (x, k) => (cterm_of (ProofContext.theory_of ctxt) (Free (x, @{typ real})), k))
fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
- List.foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty
+ (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
fun parse_cmonomial ctxt =
rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
@@ -108,7 +108,7 @@
rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
- List.foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.empty
+ (fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty)
(* positivstellensatz parser *)
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Oct 29 23:58:15 2009 +0100
@@ -526,7 +526,7 @@
fun make_intr s T (cname, cargs) =
let
- fun mk_prem (dt, (j, j', prems, ts)) =
+ fun mk_prem dt (j, j', prems, ts) =
let
val (dts, dt') = strip_option dt;
val (dts', dt'') = strip_dtyp dt';
@@ -535,7 +535,7 @@
val T = typ_of_dtyp descr sorts dt'';
val free = mk_Free "x" (Us ---> T) j;
val free' = app_bnds free (length Us);
- fun mk_abs_fun (T, (i, t)) =
+ fun mk_abs_fun T (i, t) =
let val U = fastype_of t
in (i + 1, Const ("Nominal.abs_fun", [T, U, T] --->
Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t)
@@ -546,10 +546,10 @@
HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k),
T --> HOLogic.boolT) $ free')) :: prems
| _ => prems,
- snd (List.foldr mk_abs_fun (j', free) Ts) :: ts)
+ snd (fold_rev mk_abs_fun Ts (j', free)) :: ts)
end;
- val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs;
+ val (_, _, prems, ts) = fold_rev mk_prem cargs (1, 1, [], []);
val concl = HOLogic.mk_Trueprop (Free (s, T --> HOLogic.boolT) $
list_comb (Const (cname, map fastype_of ts ---> T), ts))
in Logic.list_implies (prems, concl)
@@ -710,7 +710,7 @@
(**** constructors ****)
- fun mk_abs_fun (x, t) =
+ fun mk_abs_fun x t =
let
val T = fastype_of x;
val U = fastype_of t
@@ -776,7 +776,7 @@
fun make_constr_def tname T T' (((cname_rep, _), (cname, cargs)), (cname', mx))
(thy, defs, eqns) =
let
- fun constr_arg ((dts, dt), (j, l_args, r_args)) =
+ fun constr_arg (dts, dt) (j, l_args, r_args) =
let
val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' sorts dt) i)
(dts ~~ (j upto j + length dts - 1))
@@ -784,16 +784,16 @@
in
(j + length dts + 1,
xs @ x :: l_args,
- List.foldr mk_abs_fun
+ fold_rev mk_abs_fun xs
(case dt of
DtRec k => if k < length new_type_names then
Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt -->
typ_of_dtyp descr sorts dt) $ x
else error "nested recursion not (yet) supported"
- | _ => x) xs :: r_args)
+ | _ => x) :: r_args)
end
- val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
+ val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
val constrT = map fastype_of l_args ---> T;
@@ -902,7 +902,7 @@
let val T = fastype_of t
in Const ("Nominal.perm", permT --> T --> T) $ pi $ t end;
- fun constr_arg ((dts, dt), (j, l_args, r_args)) =
+ fun constr_arg (dts, dt) (j, l_args, r_args) =
let
val Ts = map (typ_of_dtyp descr'' sorts) dts;
val xs = map (fn (T, i) => mk_Free "x" T i)
@@ -914,7 +914,7 @@
map perm (xs @ [x]) @ r_args)
end
- val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts;
+ val (_, l_args, r_args) = fold_rev constr_arg dts (1, [], []);
val c = Const (cname, map fastype_of l_args ---> T)
in
Goal.prove_global thy8 [] []
@@ -952,7 +952,7 @@
val cname = Sign.intern_const thy8
(Long_Name.append tname (Long_Name.base_name cname));
- fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
+ fun make_inj (dts, dt) (j, args1, args2, eqs) =
let
val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
@@ -963,10 +963,10 @@
(j + length dts + 1,
xs @ (x :: args1), ys @ (y :: args2),
HOLogic.mk_eq
- (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs)
+ (fold_rev mk_abs_fun xs x, fold_rev mk_abs_fun ys y) :: eqs)
end;
- val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts;
+ val (_, args1, args2, eqs) = fold_rev make_inj dts (1, [], [], []);
val Ts = map fastype_of args1;
val c = Const (cname, Ts ---> T)
in
@@ -995,17 +995,17 @@
(Long_Name.append tname (Long_Name.base_name cname));
val atomT = Type (atom, []);
- fun process_constr ((dts, dt), (j, args1, args2)) =
+ fun process_constr (dts, dt) (j, args1, args2) =
let
val Ts_idx = map (typ_of_dtyp descr'' sorts) dts ~~ (j upto j + length dts - 1);
val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts)
in
(j + length dts + 1,
- xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2)
+ xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2)
end;
- val (_, args1, args2) = List.foldr process_constr (1, [], []) dts;
+ val (_, args1, args2) = fold_rev process_constr dts (1, [], []);
val Ts = map fastype_of args1;
val c = list_comb (Const (cname, Ts ---> T), args1);
fun supp t =
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Oct 29 23:58:15 2009 +0100
@@ -125,7 +125,7 @@
fun make_rec_intr T rec_set (cname, cargs) (rec_intr_ts, l) =
let
- fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
+ fun mk_prem (dt, U) (j, k, prems, t1s, t2s) =
let val free1 = mk_Free "x" U j
in (case (strip_dtyp dt, strip_type U) of
((_, DtRec m), (Us, _)) =>
@@ -141,7 +141,7 @@
end;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
+ val (_, _, prems, t1s, t2s) = fold_rev mk_prem (cargs ~~ Ts) (1, 1, [], [], [])
in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop
(rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Thu Oct 29 23:58:15 2009 +0100
@@ -162,8 +162,7 @@
val prem' = hd (prems_of exhaustion);
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
- cterm_of thy (List.foldr (fn ((_, T), t) => Abs ("z", T, t))
- (Bound 0) params))] exhaustion
+ cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
in compose_tac (false, exhaustion', nprems_of exhaustion) i state
end;
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Oct 29 23:58:15 2009 +0100
@@ -313,20 +313,20 @@
val (_, fs) = strip_comb comb_t;
val used = ["P", "x"] @ (map (fst o dest_Free) fs);
- fun process_constr (((cname, cargs), f), (t1s, t2s)) =
+ fun process_constr ((cname, cargs), f) (t1s, t2s) =
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
val eqn = HOLogic.mk_eq (Free ("x", T),
list_comb (Const (cname, Ts ---> T), frees));
val P' = P $ list_comb (f, frees)
- in ((List.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
- (HOLogic.imp $ eqn $ P') frees)::t1s,
- (List.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
- (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
+ in (fold_rev (fn Free (s, T) => fn t => HOLogic.mk_all (s, T, t)) frees
+ (HOLogic.imp $ eqn $ P') :: t1s,
+ fold_rev (fn Free (s, T) => fn t => HOLogic.mk_exists (s, T, t)) frees
+ (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) :: t2s)
end;
- val (t1s, t2s) = List.foldr process_constr ([], []) (constrs ~~ fs);
+ val (t1s, t2s) = fold_rev process_constr (constrs ~~ fs) ([], []);
val lhs = P $ (comb_t $ Free ("x", T))
in
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
@@ -423,9 +423,9 @@
val tnames = Name.variant_list ["v"] (make_tnames Ts);
val frees = tnames ~~ Ts
in
- List.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
+ fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
(HOLogic.mk_eq (Free ("v", T),
- list_comb (Const (cname, Ts ---> T), map Free frees))) frees
+ list_comb (Const (cname, Ts ---> T), map Free frees)))
end
in map (fn ((_, (_, _, constrs)), T) =>
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Thu Oct 29 23:58:15 2009 +0100
@@ -138,21 +138,24 @@
tname_of (body_type T) mem ["set", "bool"]) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
- val prf = List.foldr forall_intr_prf
- (List.foldr (fn ((f, p), prf) =>
- (case head_of (strip_abs_body f) of
- Free (s, T) =>
- let val T' = Logic.varifyT T
- in Abst (s, SOME T', Proofterm.prf_abstract_over
- (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
- end
- | _ => AbsP ("H", SOME p, prf)))
- (Proofterm.proof_combP
- (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
+ val prf =
+ List.foldr forall_intr_prf
+ (fold_rev (fn (f, p) => fn prf =>
+ (case head_of (strip_abs_body f) of
+ Free (s, T) =>
+ let val T' = Logic.varifyT T
+ in Abst (s, SOME T', Proofterm.prf_abstract_over
+ (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
+ end
+ | _ => AbsP ("H", SOME p, prf)))
+ (rec_fns ~~ prems_of thm)
+ (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
- val r' = if null is then r else Logic.varify (List.foldr (uncurry lambda)
- r (map Logic.unvarify ivs1 @ filter_out is_unit
- (map (head_of o strip_abs_body) rec_fns)));
+ val r' =
+ if null is then r
+ else Logic.varify (fold_rev lambda
+ (map Logic.unvarify ivs1 @ filter_out is_unit
+ (map (head_of o strip_abs_body) rec_fns)) r);
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
@@ -200,10 +203,10 @@
val P = Var (("P", 0), rT' --> HOLogic.boolT);
val prf = forall_intr_prf (y, forall_intr_prf (P,
- List.foldr (fn ((p, r), prf) =>
- forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
- prf))) (Proofterm.proof_combP (prf_of thm',
- map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
+ fold_rev (fn (p, r) => fn prf =>
+ forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p), prf)))
+ (prems ~~ rs)
+ (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
val r' = Logic.varify (Abs ("y", T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Oct 29 23:58:15 2009 +0100
@@ -73,8 +73,9 @@
val branchT = if null branchTs then HOLogic.unitT
else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
val arities = remove (op =) 0 (get_arities descr');
- val unneeded_vars = subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
- val leafTs = leafTs' @ (map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars);
+ val unneeded_vars =
+ subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
+ val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
val oldTs = Library.drop (length (hd descr), recTs);
@@ -133,7 +134,7 @@
in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
end;
- val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
+ fun mk_lim t Ts = fold_rev (fn T => fn t => Lim $ mk_fun_inj T (Abs ("x", T, t))) Ts t;
(************** generate introduction rules for representing set **********)
@@ -143,7 +144,8 @@
fun make_intr s n (i, (_, cargs)) =
let
- fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
+ fun mk_prem dt (j, prems, ts) =
+ (case strip_dtyp dt of
(dts, DtRec k) =>
let
val Ts = map (typ_of_dtyp descr' sorts) dts;
@@ -159,7 +161,7 @@
in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
end);
- val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs;
+ val (_, prems, ts) = fold_rev mk_prem cargs (1, [], []);
val concl = HOLogic.mk_Trueprop
(Free (s, UnivT') $ mk_univ_inj ts n i)
in Logic.list_implies (prems, concl)
@@ -213,7 +215,7 @@
fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) =
let
- fun constr_arg (dt, (j, l_args, r_args)) =
+ fun constr_arg dt (j, l_args, r_args) =
let val T = typ_of_dtyp descr' sorts dt;
val free_t = mk_Free "x" T j
in (case (strip_dtyp dt, strip_type T) of
@@ -223,7 +225,7 @@
| _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
end;
- val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs;
+ val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []);
val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
val abs_name = Sign.intern_const thy ("Abs_" ^ tname);
val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
@@ -387,7 +389,7 @@
val fun_congs = map (fn T => make_elim (Drule.instantiate'
[SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
- fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
+ fun prove_iso_thms ds (inj_thms, elem_thms) =
let
val (_, (tname, _, _)) = hd ds;
val induct = (#induct o the o Symtab.lookup dt_info) tname;
@@ -445,8 +447,8 @@
in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
end;
- val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms
- ([], map #3 newT_iso_axms) (tl descr);
+ val (iso_inj_thms_unfolded, iso_elem_thms) =
+ fold_rev prove_iso_thms (tl descr) ([], map #3 newT_iso_axms);
val iso_inj_thms = map snd newT_iso_inj_thms @
map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded;
--- a/src/HOL/Tools/Function/size.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML Thu Oct 29 23:58:15 2009 +0100
@@ -115,7 +115,7 @@
then HOLogic.zero
else foldl1 plus (ts @ [HOLogic.Suc_zero])
in
- List.foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
+ fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
end;
val fs = maps (fn (_, (name, _, constrs)) =>
--- a/src/HOL/Tools/TFL/post.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML Thu Oct 29 23:58:15 2009 +0100
@@ -28,7 +28,7 @@
*--------------------------------------------------------------------------*)
fun termination_goals rules =
map (Type.freeze o HOLogic.dest_Trueprop)
- (List.foldr (fn (th,A) => uncurry (union (op aconv)) (prems_of th, A)) [] rules);
+ (fold_rev (union (op aconv) o prems_of) rules []);
(*---------------------------------------------------------------------------
* Three postprocessors are applied to the definition. It
--- a/src/HOL/Tools/TFL/rules.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Thu Oct 29 23:58:15 2009 +0100
@@ -131,8 +131,7 @@
fun FILTER_DISCH_ALL P thm =
let fun check tm = P (#t (Thm.rep_cterm tm))
- in List.foldr (fn (tm,th) => if check tm then DISCH tm th else th)
- thm (chyps thm)
+ in fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
end;
(* freezeT expensive! *)
--- a/src/HOL/Tools/TFL/tfl.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Thu Oct 29 23:58:15 2009 +0100
@@ -529,7 +529,7 @@
then writeln (cat_lines ("Extractants =" ::
map (Display.string_of_thm_global thy) extractants))
else ()
- val TCs = List.foldr (uncurry (union (op aconv))) [] TCl
+ val TCs = fold_rev (union (op aconv)) TCl []
val full_rqt = WFR::TCs
val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
val R'abs = S.rand R'
--- a/src/HOL/Tools/choice_specification.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/choice_specification.ML Thu Oct 29 23:58:15 2009 +0100
@@ -120,7 +120,8 @@
val frees = OldTerm.term_frees prop
val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
orelse error "Specificaton: Only free variables of sort 'type' allowed"
- val prop_closed = List.foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
+ val prop_closed = fold_rev (fn (vname, T) => fn prop =>
+ HOLogic.mk_all (vname, T, prop)) (map dest_Free frees) prop
in
(prop_closed,frees)
end
@@ -151,7 +152,7 @@
| _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")
end
val proc_consts = map proc_const consts
- fun mk_exist (c,prop) =
+ fun mk_exist c prop =
let
val T = type_of c
val cname = Long_Name.base_name (fst (dest_Const c))
@@ -161,7 +162,7 @@
in
HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
end
- val ex_prop = List.foldr mk_exist prop proc_consts
+ val ex_prop = fold_rev mk_exist proc_consts prop
val cnames = map (fst o dest_Const) proc_consts
fun post_process (arg as (thy,thm)) =
let
--- a/src/HOL/Tools/inductive.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Thu Oct 29 23:58:15 2009 +0100
@@ -517,16 +517,17 @@
| (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
| _ => (s, NONE)));
- fun mk_prem (s, prems) = (case subst s of
- (_, SOME (t, u)) => t :: u :: prems
- | (t, _) => t :: prems);
+ fun mk_prem s prems =
+ (case subst s of
+ (_, SOME (t, u)) => t :: u :: prems
+ | (t, _) => t :: prems);
val SOME (_, i, ys, _) = dest_predicate cs params
(HOLogic.dest_Trueprop (Logic.strip_assums_concl r))
in list_all_free (Logic.strip_params r,
- Logic.list_implies (map HOLogic.mk_Trueprop (List.foldr mk_prem
- [] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))),
+ Logic.list_implies (map HOLogic.mk_Trueprop (fold_rev mk_prem
+ (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r)) []),
HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys))))
end;
@@ -549,9 +550,9 @@
(* make predicate for instantiation of abstract induction rule *)
val ind_pred = fold_rev lambda (bs @ xs) (foldr1 HOLogic.mk_conj
- (map_index (fn (i, P) => List.foldr HOLogic.mk_imp
- (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))
- (make_bool_args HOLogic.mk_not I bs i)) preds));
+ (map_index (fn (i, P) => fold_rev (curry HOLogic.mk_imp)
+ (make_bool_args HOLogic.mk_not I bs i)
+ (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
val ind_concl = HOLogic.mk_Trueprop
(HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
@@ -631,9 +632,10 @@
map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @
map (subst o HOLogic.dest_Trueprop)
(Logic.strip_assums_hyp r)
- in List.foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P)))
- (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
- (Logic.strip_params r)
+ in
+ fold_rev (fn (x, T) => fn P => HOLogic.exists_const T $ Abs (x, T, P))
+ (Logic.strip_params r)
+ (if null ps then HOLogic.true_const else foldr1 HOLogic.mk_conj ps)
end
(* make a disjunction of all introduction rules *)
--- a/src/HOL/Tools/inductive_codegen.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Oct 29 23:58:15 2009 +0100
@@ -71,8 +71,7 @@
{intros = intros |>
Symtab.update (s, (AList.update Thm.eq_thm_prop
(thm, (thyname_of s, nparms)) rules)),
- graph = List.foldr (uncurry (Graph.add_edge o pair s))
- (fold add_node (s :: cs) graph) cs,
+ graph = fold_rev (Graph.add_edge o pair s) cs (fold add_node (s :: cs) graph),
eqns = eqns} thy
end
| _ => (warn thm; thy))
--- a/src/HOL/Tools/inductive_realizer.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Oct 29 23:58:15 2009 +0100
@@ -263,8 +263,7 @@
val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
val rlz'' = fold_rev Logic.all vs2 rlz
in (name, (vs,
- if rt = Extraction.nullt then rt else
- List.foldr (uncurry lambda) rt vs1,
+ if rt = Extraction.nullt then rt else fold_rev lambda vs1 rt,
ProofRewriteRules.un_hhf_proof rlz' rlz''
(fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
end;
--- a/src/HOL/Tools/lin_arith.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Thu Oct 29 23:58:15 2009 +0100
@@ -645,9 +645,9 @@
fun filter_prems_tac_items (p : term -> bool) (terms : term list) : term list =
let
- fun filter_prems (t, (left, right)) =
- if p t then (left, right @ [t]) else (left @ right, [])
- val (left, right) = List.foldl filter_prems ([], []) terms
+ fun filter_prems t (left, right) =
+ if p t then (left, right @ [t]) else (left @ right, [])
+ val (left, right) = fold filter_prems terms ([], [])
in
right @ left
end;
--- a/src/HOL/Tools/meson.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/meson.ML Thu Oct 29 23:58:15 2009 +0100
@@ -432,7 +432,7 @@
(*Generate Horn clauses for all contrapositives of a clause. The input, th,
is a HOL disjunction.*)
-fun add_contras crules (th,hcs) =
+fun add_contras crules th hcs =
let fun rots (0,th) = hcs
| rots (k,th) = zero_var_indexes (make_horn crules th) ::
rots(k-1, assoc_right (th RS disj_comm))
@@ -443,9 +443,9 @@
(*Use "theorem naming" to label the clauses*)
fun name_thms label =
- let fun name1 (th, (k,ths)) =
+ let fun name1 th (k, ths) =
(k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
- in fn ths => #2 (List.foldr name1 (length ths, []) ths) end;
+ in fn ths => #2 (fold_rev name1 ths (length ths, [])) end;
(*Is the given disjunction an all-negative support clause?*)
fun is_negative th = forall (not o #1) (literals (prop_of th));
@@ -491,9 +491,9 @@
TRYALL_eq_assume_tac;
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
-fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
+fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
-fun size_of_subgoals st = List.foldr addconcl 0 (prems_of st);
+fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0;
(*Negation Normal Form*)
@@ -553,19 +553,19 @@
(trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
skolemize_nnf_list ctxt ths);
-fun add_clauses (th,cls) =
+fun add_clauses th cls =
let val ctxt0 = Variable.thm_context th
- val (cnfs,ctxt) = make_cnf [] th ctxt0
+ val (cnfs, ctxt) = make_cnf [] th ctxt0
in Variable.export ctxt ctxt0 cnfs @ cls end;
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
-fun make_clauses ths = sort_clauses (List.foldr add_clauses [] ths);
+fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
fun make_horns ths =
name_thms "Horn#"
- (distinct Thm.eq_thm_prop (List.foldr (add_contras clause_rules) [] ths));
+ (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
(*Could simply use nprems_of, which would count remaining subgoals -- no
discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
--- a/src/HOL/Tools/metis_tools.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Thu Oct 29 23:58:15 2009 +0100
@@ -628,15 +628,14 @@
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map =
+ fun add_thm is_conjecture ith {axioms, tfrees} : logic_map =
let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
in
{axioms = (mth, Meson.make_meta_clause ith) :: axioms,
tfrees = union (op =) tfree_lits tfrees}
end;
- val lmap0 = List.foldl (add_thm true)
- {axioms = [], tfrees = init_tfrees ctxt} cls
- val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
+ val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt}
+ val lmap = fold (add_thm false) ths (add_tfrees lmap0)
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
(*Now check for the existence of certain combinators*)
@@ -647,7 +646,7 @@
val thS = if used "c_COMBS" then [comb_S] else []
val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
val lmap' = if mode=FO then lmap
- else List.foldl (add_thm false) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
+ else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
in
(mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
end;
--- a/src/HOL/Tools/old_primrec.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML Thu Oct 29 23:58:15 2009 +0100
@@ -34,11 +34,11 @@
same type in all introduction rules*)
fun unify_consts thy cs intr_ts =
(let
- fun varify (t, (i, ts)) =
+ fun varify t (i, ts) =
let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
in (maxidx_of_term t', t'::ts) end;
- val (i, cs') = List.foldr varify (~1, []) cs;
- val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
+ val (i, cs') = fold_rev varify cs (~1, []);
+ val (i', intr_ts') = fold_rev varify intr_ts (i, []);
val rec_consts = fold Term.add_consts cs' [];
val intr_consts = fold Term.add_consts intr_ts' [];
fun unify (cname, cT) =
--- a/src/HOL/Tools/refute.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/refute.ML Thu Oct 29 23:58:15 2009 +0100
@@ -954,7 +954,7 @@
(* required for mutually recursive datatypes; those need to *)
(* be added even if they are an instance of an otherwise non- *)
(* recursive datatype *)
- fun collect_dtyp (d, acc) =
+ fun collect_dtyp d acc =
let
val dT = typ_of_dtyp descr typ_assoc d
in
@@ -962,7 +962,7 @@
DatatypeAux.DtTFree _ =>
collect_types dT acc
| DatatypeAux.DtType (_, ds) =>
- collect_types dT (List.foldr collect_dtyp acc ds)
+ collect_types dT (fold_rev collect_dtyp ds acc)
| DatatypeAux.DtRec i =>
if dT mem acc then
acc (* prevent infinite recursion *)
@@ -976,9 +976,9 @@
insert (op =) dT acc
else acc
(* collect argument types *)
- val acc_dtyps = List.foldr collect_dtyp acc_dT dtyps
+ val acc_dtyps = fold_rev collect_dtyp dtyps acc_dT
(* collect constructor types *)
- val acc_dconstrs = List.foldr collect_dtyp acc_dtyps (maps snd dconstrs)
+ val acc_dconstrs = fold_rev collect_dtyp (maps snd dconstrs) acc_dtyps
in
acc_dconstrs
end
@@ -986,7 +986,7 @@
in
(* argument types 'Ts' could be added here, but they are also *)
(* added by 'collect_dtyp' automatically *)
- collect_dtyp (DatatypeAux.DtRec index, acc)
+ collect_dtyp (DatatypeAux.DtRec index) acc
end
| NONE =>
(* not an inductive datatype, e.g. defined via "typedef" or *)
@@ -1596,8 +1596,9 @@
val Ts = Term.binder_types (Term.fastype_of t)
val t' = Term.incr_boundvars i t
in
- List.foldr (fn (T, term) => Abs ("<eta_expand>", T, term))
- (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i))
+ fold_rev (fn T => fn term => Abs ("<eta_expand>", T, term))
+ (List.take (Ts, i))
+ (Term.list_comb (t', map Bound (i-1 downto 0)))
end;
(* ------------------------------------------------------------------------- *)
@@ -2058,7 +2059,7 @@
Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
in
(* functions as graphs, i.e. as a (HOL) set of pairs "(x, y)" *)
- map (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
+ map (fn ps => fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) ps
HOLogic_empty_set) pairss
end
| Type (s, Ts) =>
@@ -2590,8 +2591,8 @@
(* interpretation list *)
val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs
(* apply 'intr' to all recursive arguments *)
- val result = List.foldl (fn (arg_i, i) =>
- interpretation_apply (i, arg_i)) intr arg_intrs
+ val result = fold (fn arg_i => fn i =>
+ interpretation_apply (i, arg_i)) arg_intrs intr
(* update 'REC_OPERATORS' *)
val _ = Array.update (arr, elem, (true, result))
in
@@ -2970,11 +2971,11 @@
"intersection: interpretation for set is not a node")
(* interpretation -> interpretaion *)
fun lfp (Node resultsets) =
- List.foldl (fn ((set, resultset), acc) =>
+ fold (fn (set, resultset) => fn acc =>
if is_subset (resultset, set) then
intersection (acc, set)
else
- acc) i_univ (i_sets ~~ resultsets)
+ acc) (i_sets ~~ resultsets) i_univ
| lfp _ =
raise REFUTE ("lfp_interpreter",
"lfp: interpretation for function is not a node")
@@ -3025,11 +3026,11 @@
"union: interpretation for set is not a node")
(* interpretation -> interpretaion *)
fun gfp (Node resultsets) =
- List.foldl (fn ((set, resultset), acc) =>
+ fold (fn (set, resultset) => fn acc =>
if is_subset (set, resultset) then
union (acc, set)
else
- acc) i_univ (i_sets ~~ resultsets)
+ acc) (i_sets ~~ resultsets) i_univ
| gfp _ =
raise REFUTE ("gfp_interpreter",
"gfp: interpretation for function is not a node")
@@ -3127,8 +3128,7 @@
val HOLogic_insert =
Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
in
- SOME (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc)
- HOLogic_empty_set pairs)
+ SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
end
| Type ("prop", []) =>
(case index_from_interpretation intr of
--- a/src/HOL/Tools/res_axioms.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Oct 29 23:58:15 2009 +0100
@@ -476,7 +476,7 @@
val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
(map Thm.term_of hyps)
val fixed = OldTerm.term_frees (concl_of st) @
- List.foldl (uncurry (union (op aconv))) [] (map OldTerm.term_frees remaining_hyps)
+ fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
--- a/src/HOL/Tools/simpdata.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/HOL/Tools/simpdata.ML Thu Oct 29 23:58:15 2009 +0100
@@ -64,8 +64,8 @@
else
let
val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
- fun mk_simp_implies Q = List.foldr (fn (R, S) =>
- Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
+ fun mk_simp_implies Q = fold_rev (fn R => fn S =>
+ Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Ps Q
val aT = TFree ("'a", HOLogic.typeS);
val x = Free ("x", aT);
val y = Free ("y", aT)
--- a/src/Provers/classical.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/Provers/classical.ML Thu Oct 29 23:58:15 2009 +0100
@@ -198,10 +198,10 @@
(*Uses introduction rules in the normal way, or on negated assumptions,
trying rules in order. *)
fun swap_res_tac rls =
- let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
+ let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls
in assume_tac ORELSE'
contr_tac ORELSE'
- biresolve_tac (List.foldr addrl [] rls)
+ biresolve_tac (fold_rev addrl rls [])
end;
(*Duplication of hazardous rules, for complete provers*)
--- a/src/Provers/typedsimp.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/Provers/typedsimp.ML Thu Oct 29 23:58:15 2009 +0100
@@ -64,12 +64,12 @@
(*If the rule proves an equality then add both forms to simp_rls
else add the rule to other_rls*)
-fun add_rule (rl, (simp_rls, other_rls)) =
+fun add_rule rl (simp_rls, other_rls) =
(simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
handle THM _ => (simp_rls, rl :: other_rls);
(*Given the list rls, return the pair (simp_rls, other_rls).*)
-fun process_rules rls = List.foldr add_rule ([],[]) rls;
+fun process_rules rls = fold_rev add_rule rls ([], []);
(*Given list of rewrite rules, return list of both forms, reject others*)
fun process_rewrites rls =
--- a/src/Pure/Proof/extraction.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Thu Oct 29 23:58:15 2009 +0100
@@ -77,12 +77,12 @@
val empty_rules : rules = {next = 0, rs = [], net = Net.empty};
-fun add_rule (r as (_, (lhs, _)), {next, rs, net} : rules) =
+fun add_rule (r as (_, (lhs, _))) ({next, rs, net} : rules) =
{next = next - 1, rs = r :: rs, net = Net.insert_term (K false)
(Envir.eta_contract lhs, (next, r)) net};
fun merge_rules ({next, rs = rs1, net} : rules) ({rs = rs2, ...} : rules) =
- List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
+ fold_rev add_rule (subtract (op =) rs1 rs2) {next = next, rs = rs1, net = net};
fun condrew thy rules procs =
let
@@ -231,7 +231,7 @@
defs, expand, prep} = ExtractionData.get thy;
in
ExtractionData.put
- {realizes_eqns = List.foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
+ {realizes_eqns = fold_rev add_rule (map (prep_eq thy) eqns) realizes_eqns,
typeof_eqns = typeof_eqns, types = types, realizers = realizers,
defs = defs, expand = expand, prep = prep} thy
end
@@ -249,7 +249,7 @@
in
ExtractionData.put
{realizes_eqns = realizes_eqns, realizers = realizers,
- typeof_eqns = List.foldr add_rule typeof_eqns eqns',
+ typeof_eqns = fold_rev add_rule eqns' typeof_eqns,
types = types, defs = defs, expand = expand, prep = prep} thy
end
@@ -359,8 +359,8 @@
in
(ExtractionData.put (if is_def then
{realizes_eqns = realizes_eqns,
- typeof_eqns = add_rule (([],
- Logic.dest_equals (prop_of (Drule.abs_def thm))), typeof_eqns),
+ typeof_eqns = add_rule ([],
+ Logic.dest_equals (prop_of (Drule.abs_def thm))) typeof_eqns,
types = types,
realizers = realizers, defs = insert Thm.eq_thm thm defs,
expand = expand, prep = prep}
@@ -458,7 +458,7 @@
val vars = vars_of prop;
val n = Int.min (length vars, length ts);
- fun add_args ((Var ((a, i), _), t), (vs', tye)) =
+ fun add_args (Var ((a, i), _), t) (vs', tye) =
if member (op =) rvs a then
let val T = etype_of thy' vs Ts t
in if T = nullT then (vs', tye)
@@ -466,7 +466,7 @@
end
else (vs', tye)
- in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
+ in fold_rev add_args (Library.take (n, vars) ~~ Library.take (n, ts)) ([], []) end;
fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
--- a/src/ZF/Tools/datatype_package.ML Thu Oct 29 23:17:35 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML Thu Oct 29 23:58:15 2009 +0100
@@ -129,7 +129,7 @@
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
(*The function variable for a single constructor*)
- fun add_case (((_, T, _), name, args, _), (opno, cases)) =
+ fun add_case ((_, T, _), name, args, _) (opno, cases) =
if Syntax.is_identifier name then
(opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
else
@@ -138,12 +138,12 @@
(*Treatment of a list of constructors, for one part
Result adds a list of terms, each a function variable with arguments*)
- fun add_case_list (con_ty_list, (opno, case_lists)) =
- let val (opno', case_list) = List.foldr add_case (opno, []) con_ty_list
+ fun add_case_list con_ty_list (opno, case_lists) =
+ let val (opno', case_list) = fold_rev add_case con_ty_list (opno, [])
in (opno', case_list :: case_lists) end;
(*Treatment of all parts*)
- val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists;
+ val (_, case_lists) = fold_rev add_case_list con_ty_lists (1, []);
(*extract the types of all the variables*)
val case_typ = maps (map (#2 o #1)) con_ty_lists ---> @{typ "i => i"};
@@ -215,7 +215,7 @@
val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
(*Treatment of all parts*)
- val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists;
+ val (_, recursor_lists) = fold_rev add_case_list rec_ty_lists (1, []);
(*extract the types of all the variables*)
val recursor_typ = maps (map (#2 o #1)) rec_ty_lists ---> @{typ "i => i"};