# HG changeset patch # User wenzelm # Date 1256857095 -3600 # Node ID 6748bd742d7a49f829aead71cd7d3b77b2368bc4 # Parent c5cd93763e714785609541f7ac9d07f8f07010de# Parent d41f77196338c70527c9095fd7a65824957b7744 merged diff -r c5cd93763e71 -r 6748bd742d7a src/FOLP/simp.ML --- 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)) diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Import/lazy_seq.ML --- 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 () => diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Import/proof_kernel.ML --- 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' diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML --- 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 *) diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Nominal/nominal_datatype.ML --- 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 = diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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) $ diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/Datatype/datatype_aux.ML --- 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; diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/Datatype/datatype_prop.ML --- 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) => diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/Datatype/datatype_realizer.ML --- 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]))))); diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- 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; diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/Function/size.ML --- 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)) => diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/TFL/post.ML --- 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 diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/TFL/rules.ML --- 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! *) diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/TFL/tfl.ML --- 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' diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/choice_specification.ML --- 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 diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/inductive.ML --- 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 *) diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/inductive_codegen.ML --- 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)) diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/inductive_realizer.ML --- 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; diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/lin_arith.ML --- 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; diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/meson.ML --- 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.*) diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/metis_tools.ML --- 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; diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/old_primrec.ML --- 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) = diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/refute.ML --- 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 ("", T, term)) - (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i)) + fold_rev (fn T => fn term => Abs ("", 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 diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/res_axioms.ML --- 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; diff -r c5cd93763e71 -r 6748bd742d7a src/HOL/Tools/simpdata.ML --- 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) diff -r c5cd93763e71 -r 6748bd742d7a src/Provers/classical.ML --- 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*) diff -r c5cd93763e71 -r 6748bd742d7a src/Provers/typedsimp.ML --- 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 = diff -r c5cd93763e71 -r 6748bd742d7a src/Pure/Proof/extraction.ML --- 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); diff -r c5cd93763e71 -r 6748bd742d7a src/ZF/Tools/datatype_package.ML --- 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"};