--- a/src/FOLP/simp.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/FOLP/simp.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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 ();
--- a/src/HOL/Import/lazy_seq.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Import/lazy_seq.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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 () =>
--- a/src/HOL/Import/proof_kernel.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Import/proof_kernel.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOL/Nominal/nominal_package.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/TFL/post.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOL/Tools/TFL/rules.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/TFL/tfl.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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);
--- a/src/HOL/Tools/datatype_aux.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/datatype_codegen.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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)
--- a/src/HOL/Tools/datatype_prop.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/datatype_prop.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOL/Tools/datatype_realizer.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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)));
--- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/function_package/scnp_solve.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/function_package/scnp_solve.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOL/Tools/function_package/size.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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)) =>
--- a/src/HOL/Tools/inductive_codegen.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/inductive_package.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOL/Tools/inductive_realizer.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/lin_arith.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/meson.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/meson.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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.*)
--- a/src/HOL/Tools/metis_tools.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/metis_tools.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/old_primrec_package.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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) =
--- a/src/HOL/Tools/recfun_codegen.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOL/Tools/record_package.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/record_package.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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 *)
--- a/src/HOL/Tools/refute.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/refute.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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 ("<eta_expand>", T, term))
+ List.foldr (fn (T, term) => Abs ("<eta_expand>", 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 #>
--- a/src/HOL/Tools/res_atp.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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))
--- a/src/HOL/Tools/res_axioms.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/res_clause.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/res_clause.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOL/Tools/res_hol_clause.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOL/Tools/res_reconstruct.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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")
--- a/src/HOL/Tools/simpdata.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/simpdata.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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);
--- a/src/HOL/Tools/specification_package.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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,
--- a/src/HOLCF/Tools/domain/domain_library.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_library.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/HOLCF/Tools/domain/domain_syntax.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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"];
--- a/src/Provers/blast.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Provers/blast.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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*)
--- a/src/Provers/clasimp.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Provers/clasimp.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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);
--- a/src/Provers/classical.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Provers/classical.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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*)
--- a/src/Provers/order.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Provers/order.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/Provers/trancl.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Provers/trancl.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/Provers/typedsimp.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Provers/typedsimp.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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 =
--- a/src/Pure/Isar/attrib.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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);
--- a/src/Pure/Isar/method.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Pure/Isar/method.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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))));
--- a/src/Pure/Isar/proof_context.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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;
--- a/src/Pure/Proof/reconstruct.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Pure/Proof/reconstruct.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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 =>
--- a/src/Pure/Tools/find_consts.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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 []
--- a/src/Pure/library.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Pure/library.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/Pure/pure_thy.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Pure/pure_thy.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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);
--- a/src/Tools/IsaPlanner/isand.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Tools/IsaPlanner/isand.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/Tools/IsaPlanner/rw_inst.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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)
--- a/src/ZF/Tools/datatype_package.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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"};
--- a/src/ZF/Tools/inductive_package.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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
--- a/src/ZF/Tools/primrec_package.ML Mon Mar 02 08:26:03 2009 +0100
+++ b/src/ZF/Tools/primrec_package.ML Mon Mar 02 10:48:22 2009 +0100
@@ -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