# HG changeset patch # User chaieb # Date 1235997243 0 # Node ID 7e440d357bc4066d074707d7d08710d608add587 # Parent 9152fc3af67fde54b6a3b4c0f07f7fde4cb2cbb6# Parent 6ffaa79c352c10a3b001474c84b5983652ad51cf Automated merge with ssh://chaieb@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle diff -r 6ffaa79c352c -r 7e440d357bc4 doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Mon Mar 02 12:33:12 2009 +0000 +++ b/doc-src/System/Thy/Basics.thy Mon Mar 02 12:34:03 2009 +0000 @@ -360,8 +360,8 @@ @{verbatim "-W"} option makes Isabelle enter a special process wrapper for interaction via an external program; the protocol is a stripped-down version of Proof General the interaction mode, see - also @{"file" "~~/src/Pure/Tools/isabelle_process.ML"} and @{"file" - "~~/src/Pure/Tools/isabelle_process.scala"}. + also @{"file" "~~/src/Pure/System/isabelle_process.ML"} and @{"file" + "~~/src/Pure/System/isabelle_process.scala"}. \medskip The @{verbatim "-S"} option makes the Isabelle process more secure by disabling some critical operations, notably runtime diff -r 6ffaa79c352c -r 7e440d357bc4 doc-src/System/Thy/document/Basics.tex --- a/doc-src/System/Thy/document/Basics.tex Mon Mar 02 12:33:12 2009 +0000 +++ b/doc-src/System/Thy/document/Basics.tex Mon Mar 02 12:34:03 2009 +0000 @@ -369,7 +369,7 @@ \verb|-W| option makes Isabelle enter a special process wrapper for interaction via an external program; the protocol is a stripped-down version of Proof General the interaction mode, see - also \hyperlink{file.~~/src/Pure/Tools/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Tools{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/Tools/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Tools{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}. + also \hyperlink{file.~~/src/Pure/System/isabelle-process.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}ML}}}} and \hyperlink{file.~~/src/Pure/System/isabelle-process.scala}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}System{\isacharslash}isabelle{\isacharunderscore}process{\isachardot}scala}}}}. \medskip The \verb|-S| option makes the Isabelle process more secure by disabling some critical operations, notably runtime diff -r 6ffaa79c352c -r 7e440d357bc4 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/FOLP/simp.ML Mon Mar 02 12:34:03 2009 +0000 @@ -433,7 +433,7 @@ val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As; val new_rws = List.concat(map mk_rew_rules thms); val rwrls = map mk_trans (List.concat(map mk_rew_rules thms)); - val anet' = foldr lhs_insert_thm anet rwrls + val anet' = List.foldr lhs_insert_thm anet rwrls in if !tracing andalso not(null new_rws) then (writeln"Adding rewrites:"; Display.prths new_rws; ()) else (); diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Import/lazy_seq.ML --- a/src/HOL/Import/lazy_seq.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Import/lazy_seq.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: HOL/Import/lazy_seq.ML - ID: $Id$ Author: Sebastian Skalberg, TU Muenchen Alternative version of lazy sequences. @@ -408,8 +407,8 @@ make (fn () => copy (f x)) end -fun EVERY fs = foldr (op THEN) succeed fs -fun FIRST fs = foldr (op ORELSE) fail fs +fun EVERY fs = List.foldr (op THEN) succeed fs +fun FIRST fs = List.foldr (op ORELSE) fail fs fun TRY f x = make (fn () => diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Import/proof_kernel.ML Mon Mar 02 12:34:03 2009 +0000 @@ -777,7 +777,7 @@ val (c,asl) = case terms of [] => raise ERR "x2p" "Bad oracle description" | (hd::tl) => (hd,tl) - val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors + val tg = List.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors in mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c)) end @@ -1840,7 +1840,7 @@ | inst_type ty1 ty2 (ty as Type(name,tys)) = Type(name,map (inst_type ty1 ty2) tys) in - foldr (fn (v,th) => + List.foldr (fn (v,th) => let val cdom = fst (dom_rng (fst (dom_rng cty))) val vty = type_of v @@ -1852,7 +1852,7 @@ end | SOME _ => raise ERR "GEN_ABS" "Bad constant" | NONE => - foldr (fn (v,th) => mk_ABS v th thy) th vlist' + List.foldr (fn (v,th) => mk_ABS v th thy) th vlist' val res = HOLThm(rens_of info',th1) val _ = message "RESULT:" val _ = if_debug pth res @@ -2020,7 +2020,7 @@ Sign.add_consts_i consts thy' end - val thy1 = foldr (fn(name,thy)=> + val thy1 = List.foldr (fn(name,thy)=> snd (get_defname thyname name thy)) thy1 names fun new_name name = fst (get_defname thyname name thy1) val names' = map (fn name => (new_name name,name,false)) names @@ -2041,7 +2041,7 @@ then quotename name else (quotename newname) ^ ": " ^ (quotename name),thy') end - val (new_names,thy') = foldr (fn(name,(names,thy)) => + val (new_names,thy') = List.foldr (fn(name,(names,thy)) => let val (name',thy') = handle_const (name,thy) in diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Nominal/nominal_package.ML Mon Mar 02 12:34:03 2009 +0000 @@ -547,10 +547,10 @@ HOLogic.mk_Trueprop (Free (List.nth (rep_set_names, k), T --> HOLogic.boolT) $ free')) :: prems | _ => prems, - snd (foldr mk_abs_fun (j', free) Ts) :: ts) + snd (List.foldr mk_abs_fun (j', free) Ts) :: ts) end; - val (_, _, prems, ts) = foldr mk_prem (1, 1, [], []) cargs; + val (_, _, prems, ts) = List.foldr mk_prem (1, 1, [], []) cargs; 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) @@ -716,7 +716,7 @@ Type ("Nominal.noption", [U])) $ x $ t end; - val (ty_idxs, _) = foldl + val (ty_idxs, _) = List.foldl (fn ((i, ("Nominal.noption", _, _)), p) => p | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr; @@ -738,7 +738,7 @@ val SOME index = AList.lookup op = ty_idxs i; val (constrs1, constrs2) = ListPair.unzip (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname))) - (foldl_map (fn (dts, dt) => + (Library.foldl_map (fn (dts, dt) => let val (dts', dt') = strip_option dt in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end) ([], cargs))) constrs) @@ -780,7 +780,7 @@ in (j + length dts + 1, xs @ x :: l_args, - foldr mk_abs_fun + List.foldr mk_abs_fun (case dt of DtRec k => if k < length new_type_names then Const (List.nth (rep_names, k), typ_of_dtyp descr'' sorts dt --> @@ -789,7 +789,7 @@ | _ => x) xs :: r_args) end - val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs; + val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs; 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; @@ -909,7 +909,7 @@ map perm (xs @ [x]) @ r_args) end - val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts; + val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) dts; val c = Const (cname, map fastype_of l_args ---> T) in Goal.prove_global thy8 [] [] @@ -958,10 +958,10 @@ (j + length dts + 1, xs @ (x :: args1), ys @ (y :: args2), HOLogic.mk_eq - (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs) + (List.foldr mk_abs_fun x xs, List.foldr mk_abs_fun y ys) :: eqs) end; - val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts; + val (_, args1, args2, eqs) = List.foldr make_inj (1, [], [], []) dts; val Ts = map fastype_of args1; val c = Const (cname, Ts ---> T) in @@ -997,10 +997,10 @@ val x = mk_Free "x" (typ_of_dtyp descr'' sorts dt) (j + length dts) in (j + length dts + 1, - xs @ (x :: args1), foldr mk_abs_fun x xs :: args2) + xs @ (x :: args1), List.foldr mk_abs_fun x xs :: args2) end; - val (_, args1, args2) = foldr process_constr (1, [], []) dts; + val (_, args1, args2) = List.foldr process_constr (1, [], []) dts; val Ts = map fastype_of args1; val c = list_comb (Const (cname, Ts ---> T), args1); fun supp t = @@ -1413,7 +1413,7 @@ val _ = warning "defining recursion combinator ..."; - val used = foldr OldTerm.add_typ_tfree_names [] recTs; + val used = List.foldr OldTerm.add_typ_tfree_names [] recTs; val (rec_result_Ts', rec_fn_Ts') = DatatypeProp.make_primrec_Ts descr' sorts used; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/TFL/post.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/TFL/post.ML - ID: $Id$ Author: Konrad Slind, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge @@ -31,7 +30,7 @@ *--------------------------------------------------------------------------*) fun termination_goals rules = map (Type.freeze o HOLogic.dest_Trueprop) - (foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules); + (List.foldr (fn (th,A) => gen_union (op aconv) (prems_of th, A)) [] rules); (*--------------------------------------------------------------------------- * Finds the termination conditions in (highly massaged) definition and diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/TFL/rules.ML Mon Mar 02 12:34:03 2009 +0000 @@ -131,7 +131,7 @@ fun FILTER_DISCH_ALL P thm = let fun check tm = P (#t (Thm.rep_cterm tm)) - in foldr (fn (tm,th) => if check tm then DISCH tm th else th) + in List.foldr (fn (tm,th) => if check tm then DISCH tm th else th) thm (chyps thm) end; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/TFL/tfl.ML Mon Mar 02 12:34:03 2009 +0000 @@ -330,7 +330,7 @@ val dummy = map (no_repeat_vars thy) pats val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats, map (fn (t,i) => (t,(i,true))) (enumerate R)) - val names = foldr OldTerm.add_term_names [] R + val names = List.foldr OldTerm.add_term_names [] R val atype = type_of(hd pats) and aname = Name.variant names "a" val a = Free(aname,atype) @@ -492,7 +492,7 @@ val tych = Thry.typecheck thy val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0 - val R = Free (Name.variant (foldr OldTerm.add_term_names [] eqns) Rname, + val R = Free (Name.variant (List.foldr OldTerm.add_term_names [] eqns) Rname, Rtype) val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0 val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM) @@ -533,7 +533,7 @@ Display.prths extractants; ()) else () - val TCs = foldr (gen_union (op aconv)) [] TCl + val TCs = List.foldr (gen_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' @@ -690,7 +690,7 @@ let val tych = Thry.typecheck thy val ty_info = Thry.induct_info thy in fn pats => - let val names = foldr OldTerm.add_term_names [] pats + let val names = List.foldr OldTerm.add_term_names [] pats val T = type_of (hd pats) val aname = Name.variant names "a" val vname = Name.variant (aname::names) "v" @@ -843,7 +843,7 @@ val (pats,TCsl) = ListPair.unzip pat_TCs_list val case_thm = complete_cases thy pats val domain = (type_of o hd) pats - val Pname = Name.variant (foldr (Library.foldr OldTerm.add_term_names) + val Pname = Name.variant (List.foldr (Library.foldr OldTerm.add_term_names) [] (pats::TCsl)) "P" val P = Free(Pname, domain --> HOLogic.boolT) val Sinduct = R.SPEC (tych P) Sinduction @@ -854,7 +854,7 @@ val cases = map (fn pat => Term.betapply (Sinduct_assumf, pat)) pats val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum) val proved_cases = map (prove_case fconst thy) tasks - val v = Free (Name.variant (foldr OldTerm.add_term_names [] (map concl proved_cases)) + val v = Free (Name.variant (List.foldr OldTerm.add_term_names [] (map concl proved_cases)) "v", domain) val vtyped = tych v diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Mar 02 12:34:03 2009 +0000 @@ -96,7 +96,7 @@ val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; - val used = foldr OldTerm.add_typ_tfree_names [] recTs; + val used = List.foldr OldTerm.add_typ_tfree_names [] recTs; val newTs = Library.take (length (hd descr), recTs); val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); @@ -140,7 +140,7 @@ end; val Ts = map (typ_of_dtyp descr' sorts) cargs; - val (_, _, prems, t1s, t2s) = foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts) + val (_, _, prems, t1s, t2s) = List.foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts) in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (rec_set $ list_comb (Const (cname, Ts ---> T), t1s) $ @@ -280,7 +280,7 @@ val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; - val used = foldr OldTerm.add_typ_tfree_names [] recTs; + val used = List.foldr OldTerm.add_typ_tfree_names [] recTs; val newTs = Library.take (length (hd descr), recTs); val T' = TFree (Name.variant used "'t", HOLogic.typeS); diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/datatype_aux.ML Mon Mar 02 12:34:03 2009 +0000 @@ -155,7 +155,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 (foldr (fn ((_, T), t) => Abs ("z", T, t)) + cterm_of thy (List.foldr (fn ((_, T), t) => Abs ("z", T, t)) (Bound 0) params))] exhaustion in compose_tac (false, exhaustion', nprems_of exhaustion) i state end; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/datatype_codegen.ML Mon Mar 02 12:34:03 2009 +0000 @@ -85,7 +85,7 @@ val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts; val T = Type (tname, dts'); val rest = mk_term_of_def gr "and " xs; - val (_, eqs) = foldl_map (fn (prfx, (cname, Ts)) => + val (_, eqs) = Library.foldl_map (fn (prfx, (cname, Ts)) => let val args = map (fn i => str ("x" ^ string_of_int i)) (1 upto length Ts) in (" | ", Pretty.blk (4, @@ -216,8 +216,8 @@ let val ts1 = Library.take (i, ts); val t :: ts2 = Library.drop (i, ts); - val names = foldr OldTerm.add_term_names - (map (fst o fst o dest_Var) (foldr OldTerm.add_term_vars [] ts1)) ts1; + val names = List.foldr OldTerm.add_term_names + (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1; val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T))); fun pcase [] [] [] gr = ([], gr) diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/datatype_prop.ML --- a/src/HOL/Tools/datatype_prop.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/datatype_prop.ML Mon Mar 02 12:34:03 2009 +0000 @@ -205,7 +205,7 @@ let val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; - val used = foldr OldTerm.add_typ_tfree_names [] recTs; + val used = List.foldr OldTerm.add_typ_tfree_names [] recTs; val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used; @@ -255,7 +255,7 @@ let val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; - val used = foldr OldTerm.add_typ_tfree_names [] recTs; + val used = List.foldr OldTerm.add_typ_tfree_names [] recTs; val newTs = Library.take (length (hd descr), recTs); val T' = TFree (Name.variant used "'t", HOLogic.typeS); @@ -302,7 +302,7 @@ let val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; - val used' = foldr OldTerm.add_typ_tfree_names [] recTs; + val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs; val newTs = Library.take (length (hd descr), recTs); val T' = TFree (Name.variant used' "'t", HOLogic.typeS); val P = Free ("P", T' --> HOLogic.boolT); @@ -319,13 +319,13 @@ val eqn = HOLogic.mk_eq (Free ("x", T), list_comb (Const (cname, Ts ---> T), frees)); val P' = P $ list_comb (f, frees) - in ((foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t)) + in ((List.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t)) (HOLogic.imp $ eqn $ P') frees)::t1s, - (foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t)) + (List.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t)) (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s) end; - val (t1s, t2s) = foldr process_constr ([], []) (constrs ~~ fs); + val (t1s, t2s) = List.foldr process_constr ([], []) (constrs ~~ fs); val lhs = P $ (comb_t $ Free ("x", T)) in (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)), @@ -422,7 +422,7 @@ val tnames = Name.variant_list ["v"] (make_tnames Ts); val frees = tnames ~~ Ts in - foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t)) + List.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t)) (HOLogic.mk_eq (Free ("v", T), list_comb (Const (cname, Ts ---> T), map Free frees))) frees end diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/datatype_realizer.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/datatype_realizer.ML - ID: $Id$ Author: Stefan Berghofer, TU Muenchen Porgram extraction from proofs involving datatypes: @@ -57,8 +56,8 @@ fun mk_all i s T t = if i mem is then list_all_free ([(s, T)], t) else t; - val (prems, rec_fns) = split_list (List.concat (snd (foldl_map - (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) => + val (prems, rec_fns) = split_list (List.concat (snd (Library.foldl_map + (fn (j, ((i, (_, _, constrs)), T)) => Library.foldl_map (fn (j, (cname, cargs)) => let val Ts = map (typ_of_dtyp descr sorts) cargs; val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts); @@ -139,8 +138,8 @@ tname_of (body_type T) mem ["set", "bool"]) ivs); val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs; - val prf = foldr forall_intr_prf - (foldr (fn ((f, p), prf) => + 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 @@ -151,7 +150,7 @@ (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2; - val r' = if null is then r else Logic.varify (foldr (uncurry lambda) + 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))); @@ -201,7 +200,7 @@ val P = Var (("P", 0), rT' --> HOLogic.boolT); val prf = forall_intr_prf (y, forall_intr_prf (P, - foldr (fn ((p, r), prf) => + List.foldr (fn ((p, r), prf) => forall_intr_prf (Logic.legacy_varify r, AbsP ("H", SOME (Logic.varify p), prf))) (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))) (prems ~~ rs))); diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Mar 02 12:34:03 2009 +0000 @@ -83,7 +83,7 @@ val branchT = if null branchTs then HOLogic.unitT else BalancedTree.make (fn (T, U) => Type ("+", [T, U])) branchTs; val arities = get_arities descr' \ 0; - val unneeded_vars = hd tyvars \\ foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs); + val unneeded_vars = hd tyvars \\ List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs); 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); @@ -143,7 +143,7 @@ in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs) end; - val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t))); + val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t))); (************** generate introduction rules for representing set **********) @@ -169,7 +169,7 @@ in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts) end); - val (_, prems, ts) = foldr mk_prem (1, [], []) cargs; + val (_, prems, ts) = List.foldr mk_prem (1, [], []) cargs; val concl = HOLogic.mk_Trueprop (Free (s, UnivT') $ mk_univ_inj ts n i) in Logic.list_implies (prems, concl) @@ -229,7 +229,7 @@ | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) end; - val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs; + val (_, l_args, r_args) = List.foldr constr_arg (1, [], []) cargs; 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); @@ -357,7 +357,7 @@ in (thy', char_thms' @ char_thms) end; - val (thy5, iso_char_thms) = apfst Theory.checkpoint (foldr make_iso_defs + val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs (add_path flat_names big_name thy4, []) (tl descr)); (* prove isomorphism properties *) @@ -447,7 +447,7 @@ in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm)) end; - val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms + val (iso_inj_thms_unfolded, iso_elem_thms) = List.foldr prove_iso_thms ([], map #3 newT_iso_axms) (tl descr); val iso_inj_thms = map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) iso_inj_thms_unfolded; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/function_package/scnp_solve.ML --- a/src/HOL/Tools/function_package/scnp_solve.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/function_package/scnp_solve.ML Mon Mar 02 12:34:03 2009 +0000 @@ -46,7 +46,7 @@ fun num_prog_pts (GP (arities, _)) = length arities ; fun num_graphs (GP (_, gs)) = length gs ; fun arity (GP (arities, gl)) i = nth arities i ; -fun ndigits (GP (arities, _)) = IntInf.log2 (foldl (op +) 0 arities) + 1 +fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1 (** Propositional formulas **) @@ -79,7 +79,7 @@ fun var_constrs (gp as GP (arities, gl)) = let val n = Int.max (num_graphs gp, num_prog_pts gp) - val k = foldl Int.max 1 arities + val k = List.foldl Int.max 1 arities (* Injective, provided a < 8, x < n, and i < k. *) fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1 diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/function_package/size.ML Mon Mar 02 12:34:03 2009 +0000 @@ -115,7 +115,7 @@ then HOLogic.zero else foldl1 plus (ts @ [HOLogic.Suc_zero]) in - foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT) + List.foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT) end; val fs = maps (fn (_, (name, _, constrs)) => diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Mar 02 12:34:03 2009 +0000 @@ -71,7 +71,7 @@ {intros = intros |> Symtab.update (s, (AList.update Thm.eq_thm_prop (thm, (thyname_of s, nparms)) rules)), - graph = foldr (uncurry (Graph.add_edge o pair s)) + graph = List.foldr (uncurry (Graph.add_edge o pair s)) (Library.foldl add_node (graph, s :: cs)) cs, eqns = eqns} thy end @@ -152,7 +152,7 @@ fun cprod ([], ys) = [] | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys); -fun cprods xss = foldr (map op :: o cprod) [[]] xss; +fun cprods xss = List.foldr (map op :: o cprod) [[]] xss; datatype mode = Mode of (int list option list * int list) * int list * mode option list; @@ -357,7 +357,7 @@ val (in_ts, out_ts) = get_args is 1 ts; val ((all_vs', eqs), in_ts') = - foldl_map check_constrt ((all_vs, []), in_ts); + Library.foldl_map check_constrt ((all_vs, []), in_ts); fun compile_prems out_ts' vs names [] gr = let @@ -365,8 +365,8 @@ (invoke_codegen thy defs dep module false) out_ts gr; val (eq_ps, gr3) = fold_map compile_eq eqs gr2; val ((names', eqs'), out_ts'') = - foldl_map check_constrt ((names, []), out_ts'); - val (nvs, out_ts''') = foldl_map distinct_v + Library.foldl_map check_constrt ((names, []), out_ts'); + val (nvs, out_ts''') = Library.foldl_map distinct_v ((names', map (fn x => (x, [x])) vs), out_ts''); val (out_ps', gr4) = fold_map (invoke_codegen thy defs dep module false) (out_ts''') gr3; @@ -383,8 +383,8 @@ select_mode_prem thy modes' vs' ps; val ps' = filter_out (equal p) ps; val ((names', eqs), out_ts') = - foldl_map check_constrt ((names, []), out_ts); - val (nvs, out_ts'') = foldl_map distinct_v + Library.foldl_map check_constrt ((names, []), out_ts); + val (nvs, out_ts'') = Library.foldl_map distinct_v ((names', map (fn x => (x, [x])) vs), out_ts'); val (out_ps, gr0) = fold_map (invoke_codegen thy defs dep module false) out_ts'' gr; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/inductive_package.ML Mon Mar 02 12:34:03 2009 +0000 @@ -517,7 +517,7 @@ (HOLogic.dest_Trueprop (Logic.strip_assums_concl r)) in list_all_free (Logic.strip_params r, - Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem + Logic.list_implies (map HOLogic.mk_Trueprop (List.foldr mk_prem [] (map HOLogic.dest_Trueprop (Logic.strip_assums_hyp r))), HOLogic.mk_Trueprop (list_comb (List.nth (preds, i), ys)))) end; @@ -541,7 +541,7 @@ (* 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) => foldr HOLogic.mk_imp + (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)); @@ -624,7 +624,7 @@ map HOLogic.mk_eq (make_args' argTs xs Ts ~~ ts) @ map (subst o HOLogic.dest_Trueprop) (Logic.strip_assums_hyp r) - in foldr (fn ((x, T), P) => HOLogic.exists_const T $ (Abs (x, T, P))) + 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) end diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/inductive_realizer.ML Mon Mar 02 12:34:03 2009 +0000 @@ -55,7 +55,7 @@ (subst_bound (Free (name, T), P), subst_bound (Free (name, T), Q)) | strip_one _ (Const ("==>", _) $ P $ Q) = (P, Q); -fun relevant_vars prop = foldr (fn +fun relevant_vars prop = List.foldr (fn (Var ((a, i), T), vs) => (case strip_type T of (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs | _ => vs) @@ -264,7 +264,7 @@ val rlz'' = fold_rev Logic.all vs2 rlz in (name, (vs, if rt = Extraction.nullt then rt else - foldr (uncurry lambda) rt vs1, + List.foldr (uncurry lambda) rt vs1, ProofRewriteRules.un_hhf_proof rlz' rlz'' (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule)))) end; @@ -315,7 +315,7 @@ fun get f = (these oo Option.map) f; val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info)); - val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) => + val (_, constrss) = Library.foldl_map (fn ((recs, dummies), (s, rs)) => if s mem rsets then let val (d :: dummies') = dummies; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/lin_arith.ML Mon Mar 02 12:34:03 2009 +0000 @@ -672,7 +672,7 @@ let fun filter_prems (t, (left, right)) = if p t then (left, right @ [t]) else (left @ right, []) - val (left, right) = foldl filter_prems ([], []) terms + val (left, right) = List.foldl filter_prems ([], []) terms in right @ left end; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/meson.ML Mon Mar 02 12:34:03 2009 +0000 @@ -92,7 +92,7 @@ | pairs => let val thy = theory_of_thm th val (tyenv,tenv) = - foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs + List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs val t_pairs = map term_pair_of (Vartab.dest tenv) val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th in th' end @@ -428,7 +428,7 @@ fun name_thms label = let fun name1 (th, (k,ths)) = (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) - in fn ths => #2 (foldr name1 (length ths, []) ths) end; + in fn ths => #2 (List.foldr name1 (length ths, []) ths) end; (*Is the given disjunction an all-negative support clause?*) fun is_negative th = forall (not o #1) (literals (prop_of th)); @@ -477,7 +477,7 @@ (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz -fun size_of_subgoals st = foldr addconcl 0 (prems_of st); +fun size_of_subgoals st = List.foldr addconcl 0 (prems_of st); (*Negation Normal Form*) @@ -544,12 +544,12 @@ (*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 (foldr add_clauses [] ths); +fun make_clauses ths = sort_clauses (List.foldr 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 (foldr (add_contras clause_rules) [] ths)); + (distinct Thm.eq_thm_prop (List.foldr (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 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/metis_tools.ML Mon Mar 02 12:34:03 2009 +0000 @@ -543,9 +543,9 @@ val all_thms_FO = forall (Meson.is_fol_term thy o prop_of) val isFO = (mode = ResAtp.Fol) orelse (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths)) - val lmap0 = foldl (add_thm true ctxt) + val lmap0 = List.foldl (add_thm true ctxt) {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls - val lmap = foldl (add_thm false ctxt) (add_tfrees lmap0) ths + val lmap = List.foldl (add_thm false ctxt) (add_tfrees lmap0) ths val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists (*Now check for the existence of certain combinators*) @@ -556,7 +556,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 isFO then lmap - else foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI) + else List.foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI) in add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap' end; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/old_primrec_package.ML --- a/src/HOL/Tools/old_primrec_package.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/old_primrec_package.ML Mon Mar 02 12:34:03 2009 +0000 @@ -37,8 +37,8 @@ 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') = foldr varify (~1, []) cs; - val (i', intr_ts') = foldr varify (i, []) intr_ts; + val (i, cs') = List.foldr varify (~1, []) cs; + val (i', intr_ts') = List.foldr varify (i, []) intr_ts; val rec_consts = fold Term.add_consts cs' []; val intr_consts = fold Term.add_consts intr_ts' []; fun unify (cname, cT) = diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/recfun_codegen.ML Mon Mar 02 12:34:03 2009 +0000 @@ -143,7 +143,7 @@ val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss)); val (fundef', gr3) = mk_fundef module' "" true eqs'' (add_edge (dname, dep) - (foldr (uncurry new_node) (del_nodes xs gr2) + (List.foldr (uncurry new_node) (del_nodes xs gr2) (map (fn k => (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) in (module', put_code module' fundef' gr3) end diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/record_package.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1778,7 +1778,7 @@ val names = map fst fields; val extN = full bname; val types = map snd fields; - val alphas_fields = foldr OldTerm.add_typ_tfree_names [] types; + val alphas_fields = List.foldr OldTerm.add_typ_tfree_names [] types; val alphas_ext = alphas inter alphas_fields; val len = length fields; val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields); @@ -1835,7 +1835,7 @@ let val (args',more) = chop_last args; fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]); fun build Ts = - foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args'))) + List.foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args'))) in if more = HOLogic.unit then build (map recT (0 upto parent_len)) @@ -2003,13 +2003,13 @@ end; val split_object_prop = - let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs + let fun ALL vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0)) end; val split_ex_prop = - let fun EX vs t = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs + let fun EX vs t = List.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0)) end; @@ -2228,7 +2228,7 @@ val init_env = (case parent of NONE => [] - | SOME (types, _) => foldr OldTerm.add_typ_tfrees [] types); + | SOME (types, _) => List.foldr OldTerm.add_typ_tfrees [] types); (* fields *) diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/refute.ML Mon Mar 02 12:34:03 2009 +0000 @@ -985,7 +985,7 @@ DatatypeAux.DtTFree _ => collect_types dT acc | DatatypeAux.DtType (_, ds) => - collect_types dT (foldr collect_dtyp acc ds) + collect_types dT (List.foldr collect_dtyp acc ds) | DatatypeAux.DtRec i => if dT mem acc then acc (* prevent infinite recursion *) @@ -999,9 +999,9 @@ insert (op =) dT acc else acc (* collect argument types *) - val acc_dtyps = foldr collect_dtyp acc_dT dtyps + val acc_dtyps = List.foldr collect_dtyp acc_dT dtyps (* collect constructor types *) - val acc_dconstrs = foldr collect_dtyp acc_dtyps + val acc_dconstrs = List.foldr collect_dtyp acc_dtyps (List.concat (map snd dconstrs)) in acc_dconstrs @@ -1102,7 +1102,7 @@ case next (maxsize-minsize) 0 0 diffs of SOME diffs' => (* merge with those types for which the size is fixed *) - SOME (snd (foldl_map (fn (ds, (T, _)) => + SOME (snd (Library.foldl_map (fn (ds, (T, _)) => case AList.lookup (op =) sizes (string_of_typ T) of (* return the fixed size *) SOME n => (ds, (T, n)) @@ -1196,7 +1196,7 @@ val _ = Output.immediate_output ("Translating term (sizes: " ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") (* translate 'u' and all axioms *) - val ((model, args), intrs) = foldl_map (fn ((m, a), t') => + val ((model, args), intrs) = Library.foldl_map (fn ((m, a), t') => let val (i, m', a') = interpret thy m a t' in @@ -1612,7 +1612,7 @@ val Ts = Term.binder_types (Term.fastype_of t) val t' = Term.incr_boundvars i t in - foldr (fn (T, term) => Abs ("", T, term)) + List.foldr (fn (T, term) => Abs ("", T, term)) (Term.list_comb (t', map Bound (i-1 downto 0))) (List.take (Ts, i)) end; @@ -1622,7 +1622,7 @@ (* int list -> int *) - fun sum xs = foldl op+ 0 xs; + fun sum xs = List.foldl op+ 0 xs; (* ------------------------------------------------------------------------- *) (* product: returns the product of a list 'xs' of integers *) @@ -1630,7 +1630,7 @@ (* int list -> int *) - fun product xs = foldl op* 1 xs; + fun product xs = List.foldl op* 1 xs; (* ------------------------------------------------------------------------- *) (* size_of_dtyp: the size of (an initial fragment of) an inductive data type *) @@ -1750,7 +1750,7 @@ (* create all constants of type 'T' *) val constants = make_constants thy model T (* interpret the 'body' separately for each constant *) - val ((model', args'), bodies) = foldl_map + val ((model', args'), bodies) = Library.foldl_map (fn ((m, a), c) => let (* add 'c' to 'bounds' *) @@ -2094,7 +2094,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 (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) + map (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) HOLogic_empty_set) pairss end | Type (s, Ts) => @@ -2286,7 +2286,7 @@ | search [] _ = () in search terms' terms end (* int * interpretation list *) - val (new_offset, intrs) = foldl_map (fn (off, t_elem) => + val (new_offset, intrs) = Library.foldl_map (fn (off, t_elem) => (* if 't_elem' existed at the previous depth, *) (* proceed recursively, otherwise map the entire *) (* subtree to "undefined" *) @@ -2352,7 +2352,7 @@ else (* mconstrs_count = length params *) let (* interpret each parameter separately *) - val ((model', args'), p_intrs) = foldl_map (fn ((m, a), p) => + val ((model', args'), p_intrs) = Library.foldl_map (fn ((m, a), p) => let val (i, m', a') = interpret thy m a p in @@ -2464,7 +2464,7 @@ end) descr (* associate constructors with corresponding parameters *) (* (int * (interpretation * interpretation) list) list *) - val (p_intrs', mc_p_intrs) = foldl_map + val (p_intrs', mc_p_intrs) = Library.foldl_map (fn (p_intrs', (idx, c_intrs)) => let val len = length c_intrs @@ -2630,7 +2630,7 @@ (* interpretation list *) val arg_intrs = map (uncurry rec_intr) rec_dtyps_intrs (* apply 'intr' to all recursive arguments *) - val result = foldl (fn (arg_i, i) => + val result = List.foldl (fn (arg_i, i) => interpretation_apply (i, arg_i)) intr arg_intrs (* update 'REC_OPERATORS' *) val _ = Array.update (arr, elem, (true, result)) @@ -2910,7 +2910,7 @@ (* of width 'size_elem' and depth 'length_list' (with 'size_list' *) (* nodes total) *) (* (int * (int * int)) list *) - val (_, lenoff_lists) = foldl_map (fn ((offsets, off), elem) => + val (_, lenoff_lists) = Library.foldl_map (fn ((offsets, off), elem) => (* corresponds to a pre-order traversal of the tree *) let val len = length offsets @@ -3004,7 +3004,7 @@ "intersection: interpretation for set is not a node") (* interpretation -> interpretaion *) fun lfp (Node resultsets) = - foldl (fn ((set, resultset), acc) => + List.foldl (fn ((set, resultset), acc) => if is_subset (resultset, set) then intersection (acc, set) else @@ -3055,7 +3055,7 @@ "union: interpretation for set is not a node") (* interpretation -> interpretaion *) fun gfp (Node resultsets) = - foldl (fn ((set, resultset), acc) => + List.foldl (fn ((set, resultset), acc) => if is_subset (set, resultset) then union (acc, set) else @@ -3158,7 +3158,7 @@ val HOLogic_insert = Const (@{const_name insert}, HOLogic_prodT --> HOLogic_setT --> HOLogic_setT) in - SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) + SOME (List.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) HOLogic_empty_set pairs) end | Type ("prop", []) => @@ -3293,8 +3293,6 @@ (* subterms that are then passed to other interpreters! *) (* ------------------------------------------------------------------------- *) - (* (theory -> theory) list *) - val setup = add_interpreter "stlc" stlc_interpreter #> add_interpreter "Pure" Pure_interpreter #> diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/res_atp.ML Mon Mar 02 12:34:03 2009 +0000 @@ -115,9 +115,9 @@ fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; val null_const_tab : const_typ list list Symtab.table = - foldl add_standard_const Symtab.empty standard_consts; + List.foldl add_standard_const Symtab.empty standard_consts; -fun get_goal_consts_typs thy = foldl (add_term_consts_typs_rm thy) null_const_tab; +fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab; (*Inserts a dummy "constant" referring to the theory name, so that relevance takes the given theory into account.*) @@ -190,7 +190,7 @@ end; (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*) -fun add_expand_pairs (x,ys) xys = foldl (fn (y,acc) => (x,y)::acc) xys ys; +fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys; fun consts_typs_of_term thy t = let val tab = add_term_consts_typs_rm thy (t, null_const_tab) @@ -250,7 +250,7 @@ | relevant (newpairs,rejects) [] = let val (newrels,more_rejects) = take_best max_new newpairs val new_consts = List.concat (map #2 newrels) - val rel_consts' = foldl add_const_typ_table rel_consts new_consts + val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts val newp = p + (1.0-p) / convergence in Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels))); @@ -376,7 +376,7 @@ fun add_single_names ((a, []), pairs) = pairs | add_single_names ((a, [th]), pairs) = (a,th)::pairs - | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths); + | add_single_names ((a, ths), pairs) = #2 (List.foldl (multi_name a) (1,pairs) ths); (*Ignore blacklisted basenames*) fun add_multi_names ((a, ths), pairs) = @@ -393,7 +393,7 @@ in app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt); filter (not o blacklisted o #2) - (foldl add_single_names (foldl add_multi_names [] mults) singles) + (List.foldl add_single_names (List.foldl add_multi_names [] mults) singles) end; fun check_named ("",th) = (warning ("No name for theorem " ^ Display.string_of_thm th); false) @@ -431,18 +431,18 @@ (* Type Classes Present in the Axiom or Conjecture Clauses *) (***************************************************************) -fun add_classes (sorts, cset) = foldl setinsert cset (List.concat sorts); +fun add_classes (sorts, cset) = List.foldl setinsert cset (List.concat sorts); (*Remove this trivial type class*) fun delete_type cset = Symtab.delete_safe "HOL.type" cset; fun tvar_classes_of_terms ts = let val sorts_list = map (map #2 o OldTerm.term_tvars) ts - in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end; + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; fun tfree_classes_of_terms ts = let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts - in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end; + in Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list)) end; (*fold type constructors*) fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/res_axioms.ML Mon Mar 02 12:34:03 2009 +0000 @@ -494,7 +494,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) @ - foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps) + List.foldl (gen_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 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/res_clause.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Author: Jia Meng, Cambridge University Computer Laboratory - ID: $Id$ Copyright 2004 University of Cambridge Storing/printing FOL clauses and arity clauses. @@ -95,7 +94,7 @@ val tconst_prefix = "tc_"; val class_prefix = "class_"; -fun union_all xss = foldl (op union) [] xss; +fun union_all xss = List.foldl (op union) [] xss; (*Provide readable names for the more common symbolic functions*) val const_trans_table = @@ -275,7 +274,7 @@ | pred_of_sort (LTFree (s,ty)) = (s,1) (*Given a list of sorted type variables, return a list of type literals.*) -fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts); +fun add_typs Ts = List.foldl (op union) [] (map sorts_on_typs Ts); (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a @@ -338,8 +337,8 @@ let val class_less = Sorts.class_less(Sign.classes_of thy) fun add_super sub (super,pairs) = if class_less (sub,super) then (sub,super)::pairs else pairs - fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers - in foldl add_supers [] subs end; + fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers + in List.foldl add_supers [] subs end; fun make_classrelClause (sub,super) = ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super, @@ -375,7 +374,7 @@ fun add_class tycon (class,pairs) = (class, domain_sorts(tycon,class))::pairs handle Sorts.CLASS_ERROR _ => pairs - fun try_classes tycon = (tycon, foldl (add_class tycon) [] classes) + fun try_classes tycon = (tycon, List.foldl (add_class tycon) [] classes) in map try_classes tycons end; (*Proving one (tycon, class) membership may require proving others, so iterate.*) @@ -398,7 +397,7 @@ (*FIXME: multiple-arity checking doesn't work, as update_new is the wrong function (it flags repeated declarations of a function, even with the same arity)*) -fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs; +fun update_many (tab, keypairs) = List.foldl (uncurry Symtab.update) tab keypairs; fun add_type_sort_preds (T, preds) = update_many (preds, map pred_of_sort (sorts_on_typs T)); @@ -412,14 +411,14 @@ fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) = let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits) fun upd (class,preds) = Symtab.update (class,1) preds - in foldl upd preds classes end; + in List.foldl upd preds classes end; (*** Find occurrences of functions in clauses ***) fun add_foltype_funcs (AtomV _, funcs) = funcs | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs | add_foltype_funcs (Comp(a,tys), funcs) = - foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; + List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; (*TFrees are recorded as constants*) fun add_type_sort_funcs (TVar _, funcs) = funcs diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/res_hol_clause.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,4 +1,4 @@ -(* ID: $Id$ +(* Author: Jia Meng, NICTA FOL clauses translated from HOL formulae. @@ -183,7 +183,7 @@ if isTaut cls then pairs else (name,cls)::pairs end; -fun make_axiom_clauses dfg thy = foldl (add_axiom_clause dfg thy) []; +fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) []; fun make_conjecture_clauses_aux dfg _ _ [] = [] | make_conjecture_clauses_aux dfg thy n (th::ths) = @@ -328,7 +328,7 @@ (** For DFG format: accumulate function and predicate declarations **) -fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars; +fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars; fun add_decls cma cnh (CombConst(c,tp,tvars), (funcs,preds)) = if c = "equal" then (addtypes tvars funcs, preds) @@ -347,28 +347,28 @@ fun add_literal_decls cma cnh (Literal(_,c), decls) = add_decls cma cnh (c,decls); fun add_clause_decls cma cnh (Clause {literals, ...}, decls) = - foldl (add_literal_decls cma cnh) decls literals + List.foldl (add_literal_decls cma cnh) decls literals handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") fun decls_of_clauses cma cnh clauses arity_clauses = let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab) val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty - val (functab,predtab) = (foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses) + val (functab,predtab) = (List.foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses) in - (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses), + (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses), Symtab.dest predtab) end; fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = - foldl RC.add_type_sort_preds preds ctypes_sorts + List.foldl RC.add_type_sort_preds preds ctypes_sorts handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") (*Higher-order clauses have only the predicates hBOOL and type classes.*) fun preds_of_clauses clauses clsrel_clauses arity_clauses = Symtab.dest - (foldl RC.add_classrelClause_preds - (foldl RC.add_arityClause_preds - (foldl add_clause_preds Symtab.empty clauses) + (List.foldl RC.add_classrelClause_preds + (List.foldl RC.add_arityClause_preds + (List.foldl add_clause_preds Symtab.empty clauses) arity_clauses) clsrel_clauses) @@ -390,10 +390,10 @@ fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); -fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals; +fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals; fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) = - if axiom_name mem_string user_lemmas then foldl count_literal ct literals + if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals else ct; fun cnf_helper_thms thy = @@ -402,8 +402,8 @@ fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) = if isFO then [] (*first-order*) else - let val ct0 = foldl count_clause init_counters conjectures - val ct = foldl (count_user_clause user_lemmas) ct0 axclauses + let val ct0 = List.foldl count_clause init_counters conjectures + val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses fun needed c = valOf (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K]) @@ -468,7 +468,7 @@ val helper_clauses = get_helper_clauses false thy isFO (conjectures, axclauses, user_lemmas) val (const_min_arity, const_needs_hBOOL) = count_constants (conjectures, axclauses, helper_clauses); val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_min_arity const_needs_hBOOL) conjectures) - val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss) + val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss) val out = TextIO.openOut filename in List.app (curry TextIO.output out o #1 o (clause2tptp const_min_arity const_needs_hBOOL)) axclauses; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/res_reconstruct.ML Mon Mar 02 12:34:03 2009 +0000 @@ -51,7 +51,7 @@ fun atom x = Br(x,[]); fun scons (x,y) = Br("cons", [x,y]); -val listof = foldl scons (atom "nil"); +val listof = List.foldl scons (atom "nil"); (*Strings enclosed in single quotes, e.g. filenames*) val quoted = $$"'" |-- Scan.repeat (~$$"'") --| $$"'" >> implode; @@ -243,7 +243,7 @@ fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t; fun ints_of_stree_aux (Int n, ns) = n::ns - | ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts; + | ints_of_stree_aux (Br(_,ts), ns) = List.foldl ints_of_stree_aux ns ts; fun ints_of_stree t = ints_of_stree_aux (t, []); @@ -362,7 +362,7 @@ fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; fun replace_deps (old:int, new) (lno, t, deps) = - (lno, t, foldl (op union_int) [] (map (replace_dep (old, new)) deps)); + (lno, t, List.foldl (op union_int) [] (map (replace_dep (old, new)) deps)); (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ only in type information.*) @@ -392,7 +392,7 @@ then delete_dep lno lines else (lno, t, []) :: lines | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines -and delete_dep lno lines = foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines); +and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines); fun bad_free (Free (a,_)) = String.isPrefix "sko_" a | bad_free _ = false; @@ -435,11 +435,11 @@ val tuples = map (dest_tstp o tstp_line o explode) cnfs val _ = trace (Int.toString (length tuples) ^ " tuples extracted\n") val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt - val raw_lines = foldr add_prfline [] (decode_tstp_list ctxt tuples) + val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples) val _ = trace (Int.toString (length raw_lines) ^ " raw_lines extracted\n") - val nonnull_lines = foldr add_nonnull_prfline [] raw_lines + val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") - val (_,lines) = foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines + val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines val _ = trace (Int.toString (length lines) ^ " lines extracted\n") val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n") diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/simpdata.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: HOL/simpdata.ML - ID: $Id$ Author: Tobias Nipkow Copyright 1991 University of Cambridge @@ -65,7 +64,7 @@ else let val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); - fun mk_simp_implies Q = foldr (fn (R, S) => + fun mk_simp_implies Q = List.foldr (fn (R, S) => Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps val aT = TFree ("'a", HOLogic.typeS); val x = Free ("x", aT); diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOL/Tools/specification_package.ML Mon Mar 02 12:34:03 2009 +0000 @@ -120,7 +120,7 @@ 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 = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees) + val prop_closed = List.foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees) in (prop_closed,frees) end @@ -161,7 +161,7 @@ in HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop)) end - val ex_prop = foldr mk_exist prop proc_consts + val ex_prop = List.foldr mk_exist prop proc_consts val cnames = map (fst o dest_Const) proc_consts fun post_process (arg as (thy,thm)) = let diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: HOLCF/Tools/domain/domain_axioms.ML - ID: $Id$ Author: David von Oheimb Syntax generator for domain command. @@ -29,7 +28,7 @@ val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); val when_def = ("when_def",%%:(dname^"_when") == - foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => + List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); val copy_def = let @@ -37,7 +36,7 @@ then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x) else Bound(z-x); fun one_con (con,args) = - foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args; + List.foldr /\# (list_ccomb (%%:con, mapn (idxs (length args)) 1 args)) args; in ("copy_def", %%:(dname^"_copy") == /\ "f" (list_ccomb (%%:(dname^"_when"), map one_con cons))) end; @@ -49,7 +48,7 @@ fun inj y 1 _ = y | inj y _ 0 = mk_sinl y | inj y i j = mk_sinr (inj y (i-1) (j-1)); - in foldr /\# (dc_abs`(inj (parms args) m n)) args end; + in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; val con_defs = mapn (fn n => fn (con,args) => (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; @@ -57,14 +56,14 @@ val dis_defs = let fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (foldr /\# + (fn (con',args) => (List.foldr /\# (if con'=con then TT else FF) args)) cons)) in map ddef cons end; val mat_defs = let fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (foldr /\# + (fn (con',args) => (List.foldr /\# (if con'=con then mk_return (mk_ctuple (map (bound_arg args) args)) else mk_fail) args)) cons)) @@ -79,7 +78,7 @@ val r = Bound (length args); val rhs = case args of [] => mk_return HOLogic.unit | _ => mk_ctuple_pat ps ` mk_ctuple xs; - fun one_con (con',args') = foldr /\# (if con'=con then rhs else mk_fail) args'; + fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == list_ccomb(%%:(dname^"_when"), map one_con cons)) end @@ -89,7 +88,7 @@ fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == list_ccomb(%%:(dname^"_when"),map (fn (con',args) => if con'<>con then UU else - foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); + List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; @@ -152,11 +151,11 @@ (allargs~~((allargs_cnt-1) downto 0))); fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); - val capps = foldr mk_conj (mk_conj( + val capps = List.foldr mk_conj (mk_conj( Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) (mapn rel_app 1 rec_args); - in foldr mk_ex (Library.foldr mk_conj + in List.foldr mk_ex (Library.foldr mk_conj (map (defined o Bound) nonlazy_idxs,capps)) allvns end; fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( proj (Bound 2) eqs n $ Bound 1 $ Bound 0, diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOLCF/Tools/domain/domain_library.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: HOLCF/Tools/domain/domain_library.ML - ID: $Id$ Author: David von Oheimb Library for domain command. @@ -15,7 +14,7 @@ | itr [a] = f2 a | itr (a::l) = f(a, itr l) in itr l end; -fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => +fun map_cumulr f start xs = List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => (y::ys,res2)) ([],start) xs; diff -r 6ffaa79c352c -r 7e440d357bc4 src/HOLCF/Tools/domain/domain_syntax.ML --- a/src/HOLCF/Tools/domain/domain_syntax.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: HOLCF/Tools/domain/domain_syntax.ML - ID: $Id$ Author: David von Oheimb Syntax generator for domain command. @@ -22,14 +21,14 @@ else foldr1 mk_sprodT (map opt_lazy args); fun freetvar s = let val tvar = mk_TFree s in if tvar mem typevars then freetvar ("t"^s) else tvar end; - fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args); + fun when_type (_ ,_,args) = List.foldr (op ->>) (freetvar "t") (map third args); in val dtype = Type(dname,typevars); val dtype2 = foldr1 mk_ssumT (map prod cons'); val dnam = Sign.base_name dname; val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); - val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); + val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn); end; @@ -41,7 +40,7 @@ else c::esc cs | esc [] = [] in implode o esc o Symbol.explode end; - fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s); + fun con (name,s,args) = (name, List.foldr (op ->>) dtype (map third args),s); fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT, Mixfix(escape ("is_" ^ con), [], Syntax.max_pri)); (* strictly speaking, these constants have one argument, @@ -86,7 +85,7 @@ val capp = app "Rep_CFun"; fun con1 n (con,mx,args) = Library.foldl capp (c_ast con mx, argvars n args); fun case1 n (con,mx,args) = app "_case1" (con1 n (con,mx,args), expvar n); - fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args); + fun arg1 n (con,_,args) = List.foldr cabs (expvar n) (argvars n args); fun when1 n m = if n = m then arg1 n else K (Constant "UU"); fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; diff -r 6ffaa79c352c -r 7e440d357bc4 src/Provers/blast.ML --- a/src/Provers/blast.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Provers/blast.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: Provers/blast.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge @@ -764,8 +763,8 @@ end (*substitute throughout "stack frame"; extract affected formulae*) fun subFrame ((Gs,Hs), (changed, frames)) = - let val (changed', Gs') = foldr subForm (changed, []) Gs - val (changed'', Hs') = foldr subForm (changed', []) Hs + let val (changed', Gs') = List.foldr subForm (changed, []) Gs + val (changed'', Hs') = List.foldr subForm (changed', []) Hs in (changed'', (Gs',Hs')::frames) end (*substitute throughout literals; extract affected ones*) fun subLit (lit, (changed, nlits)) = @@ -773,8 +772,8 @@ in if nlit aconv lit then (changed, nlit::nlits) else ((nlit,true)::changed, nlits) end - val (changed, lits') = foldr subLit ([], []) lits - val (changed', pairs') = foldr subFrame (changed, []) pairs + val (changed, lits') = List.foldr subLit ([], []) lits + val (changed', pairs') = List.foldr subFrame (changed, []) pairs in if !trace then writeln ("Substituting " ^ traceTerm thy u ^ " for " ^ traceTerm thy t ^ " in branch" ) else (); @@ -971,7 +970,7 @@ then lim - (1+log(length rules)) else lim (*discourage branching updates*) val vars = vars_in_vars vars - val vars' = foldr add_terms_vars vars prems + val vars' = List.foldr add_terms_vars vars prems val choices' = (ntrl, nbrs, PRV) :: choices val tacs' = (tac(updated,false,true)) :: tacs (*no duplication; rotate*) @@ -1098,7 +1097,7 @@ then let val updated = ntrl < !ntrail (*branch updated*) val vars = vars_in_vars vars - val vars' = foldr add_terms_vars vars prems + val vars' = List.foldr add_terms_vars vars prems (*duplicate H if md permits*) val dup = md (*earlier had "andalso vars' <> vars": duplicate only if the subgoal has new vars*) diff -r 6ffaa79c352c -r 7e440d357bc4 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Provers/clasimp.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: Provers/clasimp.ML - ID: $Id$ Author: David von Oheimb, TU Muenchen Combination of classical reasoner and simplifier (depends on @@ -153,7 +152,7 @@ end; fun modifier att (x, ths) = - fst (foldl_map (Library.apply [att]) (x, rev ths)); + fst (Library.foldl_map (Library.apply [att]) (x, rev ths)); val addXIs = modifier (ContextRules.intro_query NONE); val addXEs = modifier (ContextRules.elim_query NONE); diff -r 6ffaa79c352c -r 7e440d357bc4 src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Provers/classical.ML Mon Mar 02 12:34:03 2009 +0000 @@ -223,7 +223,7 @@ let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in assume_tac ORELSE' contr_tac ORELSE' - biresolve_tac (foldr addrl [] rls) + biresolve_tac (List.foldr addrl [] rls) end; (*Duplication of hazardous rules, for complete provers*) diff -r 6ffaa79c352c -r 7e440d357bc4 src/Provers/order.ML --- a/src/Provers/order.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Provers/order.ML Mon Mar 02 12:34:03 2009 +0000 @@ -639,7 +639,7 @@ (* Compute, for each adjacency list, the list with reversed edges, and concatenate these lists. *) - val flipped = foldr (op @) nil (map flip g) + val flipped = List.foldr (op @) nil (map flip g) in assemble g flipped end @@ -677,7 +677,7 @@ let val _ = visited := u :: !visited val descendents = - foldr (fn ((v,l),ds) => if been_visited v then ds + List.foldr (fn ((v,l),ds) => if been_visited v then ds else v :: dfs_visit g v @ ds) nil (adjacent (op aconv) g u) in @@ -727,7 +727,7 @@ let val _ = visited := u :: !visited val descendents = - foldr (fn ((v,l),ds) => if been_visited v then ds + List.foldr (fn ((v,l),ds) => if been_visited v then ds else v :: dfs_visit g v @ ds) nil (adjacent (op =) g u) in descendents end diff -r 6ffaa79c352c -r 7e440d357bc4 src/Provers/trancl.ML --- a/src/Provers/trancl.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Provers/trancl.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,8 +1,6 @@ (* - Title: Transitivity reasoner for transitive closures of relations - Id: $Id$ - Author: Oliver Kutter - Copyright: TU Muenchen + Title: Transitivity reasoner for transitive closures of relations + Author: Oliver Kutter, TU Muenchen *) (* @@ -335,7 +333,7 @@ (* Compute, for each adjacency list, the list with reversed edges, and concatenate these lists. *) - val flipped = foldr (op @) nil (map flip g) + val flipped = List.foldr (op @) nil (map flip g) in assemble g flipped end @@ -359,7 +357,7 @@ let val _ = visited := u :: !visited val descendents = - foldr (fn ((v,l),ds) => if been_visited v then ds + List.foldr (fn ((v,l),ds) => if been_visited v then ds else v :: dfs_visit g v @ ds) nil (adjacent eq_comp g u) in descendents end diff -r 6ffaa79c352c -r 7e440d357bc4 src/Provers/typedsimp.ML --- a/src/Provers/typedsimp.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Provers/typedsimp.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: typedsimp - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -70,7 +69,7 @@ handle THM _ => (simp_rls, rl :: other_rls); (*Given the list rls, return the pair (simp_rls, other_rls).*) -fun process_rules rls = foldr add_rule ([],[]) rls; +fun process_rules rls = List.foldr add_rule ([],[]) rls; (*Given list of rewrite rules, return list of both forms, reject others*) fun process_rewrites rls = diff -r 6ffaa79c352c -r 7e440d357bc4 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Pure/Isar/attrib.ML Mon Mar 02 12:34:03 2009 +0000 @@ -198,7 +198,7 @@ let val ths = Facts.select thmref fact; val atts = map (attribute_i thy) srcs; - val (context', ths') = foldl_map (Library.apply atts) (context, ths); + val (context', ths') = Library.foldl_map (Library.apply atts) (context, ths); in (context', pick name ths') end) end); diff -r 6ffaa79c352c -r 7e440d357bc4 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Pure/Isar/method.ML Mon Mar 02 12:34:03 2009 +0000 @@ -436,7 +436,7 @@ local fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; -fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths); +fun app (f, att) (context, ths) = Library.foldl_map att (Context.map_proof f context, ths); fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- (fn (m, ths) => Scan.succeed (app m (context, ths)))); diff -r 6ffaa79c352c -r 7e440d357bc4 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Pure/Isar/proof_context.ML Mon Mar 02 12:34:03 2009 +0000 @@ -975,7 +975,7 @@ val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts); fun app (th, attrs) x = - swap (foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th)); + swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th)); val (res, ctxt') = fold_map app facts ctxt; val thms = PureThy.name_thms false false pos name (flat res); val Mode {stmt, ...} = get_mode ctxt; diff -r 6ffaa79c352c -r 7e440d357bc4 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Pure/Proof/reconstruct.ML Mon Mar 02 12:34:03 2009 +0000 @@ -106,7 +106,7 @@ fun decompose thy Ts (env, p as (t, u)) = let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p - else apsnd flat (foldl_map (decompose thy Ts) (uT env T U, ts ~~ us)) + else apsnd flat (Library.foldl_map (decompose thy Ts) (uT env T U, ts ~~ us)) in case pairself (strip_comb o Envir.head_norm env) p of ((Const c, ts), (Const d, us)) => rigrig c d (unifyT thy) ts us | ((Free c, ts), (Free d, us)) => rigrig c d (unifyT thy) ts us @@ -141,7 +141,7 @@ val tvars = OldTerm.term_tvars prop; val tfrees = OldTerm.term_tfrees prop; val (env', Ts) = (case opTs of - NONE => foldl_map mk_tvar (env, map snd tvars @ map snd tfrees) + NONE => Library.foldl_map mk_tvar (env, map snd tvars @ map snd tfrees) | SOME Ts => (env, Ts)); val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) (forall_intr_vfs prop) handle Library.UnequalLengths => diff -r 6ffaa79c352c -r 7e440d357bc4 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Pure/Tools/find_consts.ML Mon Mar 02 12:34:03 2009 +0000 @@ -111,7 +111,7 @@ val criteria = map make_criterion (! default_criteria @ raw_criteria); val (_, consts) = (#constants o Consts.dest o Sign.consts_of) thy; - fun eval_entry c = foldl filter_const (SOME (c, low_ranking)) criteria; + fun eval_entry c = List.foldl filter_const (SOME (c, low_ranking)) criteria; val matches = Symtab.fold (cons o eval_entry) consts [] diff -r 6ffaa79c352c -r 7e440d357bc4 src/Pure/library.ML --- a/src/Pure/library.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Pure/library.ML Mon Mar 02 12:34:03 2009 +0000 @@ -76,7 +76,6 @@ val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a - val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list val flat: 'a list list -> 'a list val unflat: 'a list list -> 'b list -> 'b list list val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list @@ -238,6 +237,7 @@ include BASIC_LIBRARY val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b + val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list val take: int * 'a list -> 'a list val drop: int * 'a list -> 'a list val last_elem: 'a list -> 'a diff -r 6ffaa79c352c -r 7e440d357bc4 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Pure/pure_thy.ML Mon Mar 02 12:34:03 2009 +0000 @@ -177,7 +177,7 @@ fun add_thms_atts pre_name ((b, thms), atts) = enter_thms pre_name (name_thms false true Position.none) - (foldl_map (Thm.theory_attributes atts)) (b, thms); + (Library.foldl_map (Thm.theory_attributes atts)) (b, thms); fun gen_add_thmss pre_name = fold_map (add_thms_atts pre_name); @@ -207,9 +207,9 @@ val name = Sign.full_name thy b; val _ = Position.report (Markup.fact_decl name) pos; - fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths); + fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths); val (thms, thy') = thy |> enter_thms - (name_thmss true pos) (name_thms false true pos) (apsnd flat o foldl_map app) + (name_thmss true pos) (name_thms false true pos) (apsnd flat o Library.foldl_map app) (b, map (fn (ths, atts) => (ths, surround tag (atts @ more_atts))) ths_atts); in ((name, thms), thy') end); diff -r 6ffaa79c352c -r 7e440d357bc4 src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Tools/IsaPlanner/isand.ML Mon Mar 02 12:34:03 2009 +0000 @@ -132,7 +132,7 @@ fun allify_prem_var (vt as (n,ty),t) = (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) - fun allify_prem Ts p = foldr allify_prem_var p Ts + fun allify_prem Ts p = List.foldr allify_prem_var p Ts val cTs = map (ctermify o Free) Ts val cterm_asms = map (ctermify o allify_prem Ts) premts @@ -306,7 +306,7 @@ in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end; fun allify_for_sg_term ctermify vs t = - let val t_alls = foldr allify_term t vs; + let val t_alls = List.foldr allify_term t vs; val ct_alls = ctermify t_alls; in (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) @@ -394,7 +394,7 @@ |> Drule.forall_intr_list cfvs in Drule.compose_single (solth', i, gth) end; -fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs; +fun export_solutions (xs,th) = List.foldr (uncurry export_solution) th xs; (* fix parameters of a subgoal "i", as free variables, and create an diff -r 6ffaa79c352c -r 7e440d357bc4 src/Tools/IsaPlanner/rw_inst.ML --- a/src/Tools/IsaPlanner/rw_inst.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/Tools/IsaPlanner/rw_inst.ML Mon Mar 02 12:34:03 2009 +0000 @@ -136,7 +136,7 @@ fun mk_renamings tgt rule_inst = let val rule_conds = Thm.prems_of rule_inst - val names = foldr OldTerm.add_term_names [] (tgt :: rule_conds); + val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds); val (conds_tyvs,cond_vs) = Library.foldl (fn ((tyvs, vs), t) => (Library.union @@ -147,7 +147,7 @@ val termvars = map Term.dest_Var (OldTerm.term_vars tgt); val vars_to_fix = Library.union (termvars, cond_vs); val (renamings, names2) = - foldr (fn (((n,i),ty), (vs, names')) => + List.foldr (fn (((n,i),ty), (vs, names')) => let val n' = Name.variant names' n in ((((n,i),ty), Free (n', ty)) :: vs, n'::names') end) @@ -166,13 +166,13 @@ let val ignore_ixs = map fst ignore_insts; val (tvars, tfrees) = - foldr (fn (t, (varixs, tfrees)) => + List.foldr (fn (t, (varixs, tfrees)) => (OldTerm.add_term_tvars (t,varixs), OldTerm.add_term_tfrees (t,tfrees))) ([],[]) ts; val unfixed_tvars = List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars; - val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars + val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars in (fixtyinsts, tfrees) end; @@ -248,7 +248,7 @@ Ts; (* type-instantiate the var instantiations *) - val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => + val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) => (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t)) :: insts_tyinst) diff -r 6ffaa79c352c -r 7e440d357bc4 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/ZF/Tools/datatype_package.ML Mon Mar 02 12:34:03 2009 +0000 @@ -1,5 +1,4 @@ (* Title: ZF/Tools/datatype_package.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge @@ -140,11 +139,11 @@ (*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) = foldr add_case (opno, []) con_ty_list + let val (opno', case_list) = List.foldr add_case (opno, []) con_ty_list in (opno', case_list :: case_lists) end; (*Treatment of all parts*) - val (_, case_lists) = foldr add_case_list (1,[]) con_ty_lists; + val (_, case_lists) = List.foldr add_case_list (1,[]) con_ty_lists; (*extract the types of all the variables*) val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"}; @@ -184,7 +183,7 @@ val rec_args = map (make_rec_call (rev case_args,0)) (List.drop(recursor_args, ncase_args)) in - foldr add_abs + List.foldr add_abs (list_comb (recursor_var, bound_args @ rec_args)) case_args end @@ -216,7 +215,7 @@ val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); (*Treatment of all parts*) - val (_, recursor_lists) = foldr add_case_list (1,[]) rec_ty_lists; + val (_, recursor_lists) = List.foldr add_case_list (1,[]) rec_ty_lists; (*extract the types of all the variables*) val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"}; diff -r 6ffaa79c352c -r 7e440d357bc4 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/ZF/Tools/inductive_package.ML Mon Mar 02 12:34:03 2009 +0000 @@ -99,7 +99,7 @@ Syntax.string_of_term ctxt t); (*** Construct the fixedpoint definition ***) - val mk_variant = Name.variant (foldr OldTerm.add_term_names [] intr_tms); + val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms); val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; @@ -113,7 +113,7 @@ val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds val exfrees = OldTerm.term_frees intr \\ rec_params val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr)) - in foldr FOLogic.mk_exists + in List.foldr FOLogic.mk_exists (BalancedTree.make FOLogic.mk_conj (zeq::prems)) exfrees end; @@ -303,7 +303,7 @@ (*Make a premise of the induction rule.*) fun induct_prem ind_alist intr = let val quantfrees = map dest_Free (OldTerm.term_frees intr \\ rec_params) - val iprems = foldr (add_induct_prem ind_alist) [] + val iprems = List.foldr (add_induct_prem ind_alist) [] (Logic.strip_imp_prems intr) val (t,X) = Ind_Syntax.rule_concl intr val (SOME pred) = AList.lookup (op aconv) ind_alist X @@ -380,7 +380,7 @@ val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name, elem_factors ---> FOLogic.oT) val qconcl = - foldr FOLogic.mk_all + List.foldr FOLogic.mk_all (FOLogic.imp $ (@{const mem} $ elem_tuple $ rec_tm) $ (list_comb (pfree, elem_frees))) elem_frees diff -r 6ffaa79c352c -r 7e440d357bc4 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Mon Mar 02 12:33:12 2009 +0000 +++ b/src/ZF/Tools/primrec_package.ML Mon Mar 02 12:34:03 2009 +0000 @@ -120,7 +120,7 @@ | SOME (rhs, cargs', eq) => (rhs, inst_recursor (recursor_pair, cargs'), eq) val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs)) - val abs = foldr absterm rhs allowed_terms + val abs = List.foldr absterm rhs allowed_terms in if !Ind_Syntax.trace then writeln ("recursor_rhs = " ^ @@ -145,7 +145,7 @@ val def_tm = Logic.mk_equals (subst_bound (rec_arg, fabs), list_comb (recursor, - foldr add_case [] (cnames ~~ recursor_pairs)) + List.foldr add_case [] (cnames ~~ recursor_pairs)) $ rec_arg) in @@ -164,7 +164,7 @@ let val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args); val SOME (fname, ftype, ls, rs, con_info, eqns) = - foldr (process_eqn thy) NONE eqn_terms; + List.foldr (process_eqn thy) NONE eqn_terms; val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); val ([def_thm], thy1) = thy