# HG changeset patch # User wenzelm # Date 1256856993 -3600 # Node ID d41f77196338c70527c9095fd7a65824957b7744 # Parent de76079f973a50098d84ee31c37f365bd474b87e eliminated some old folds; diff -r de76079f973a -r d41f77196338 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/FOLP/simp.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Import/lazy_seq.ML --- a/src/HOL/Import/lazy_seq.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Import/lazy_seq.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Import/proof_kernel.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/Function/size.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/choice_specification.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/lin_arith.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/meson.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/metis_tools.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/refute.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/res_axioms.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/HOL/Tools/simpdata.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/Provers/classical.ML --- a/src/Provers/classical.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/Provers/classical.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/Provers/typedsimp.ML --- a/src/Provers/typedsimp.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/Provers/typedsimp.ML Thu Oct 29 23:56:33 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 de76079f973a -r d41f77196338 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Thu Oct 29 23:49:55 2009 +0100 +++ b/src/ZF/Tools/datatype_package.ML Thu Oct 29 23:56:33 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"};