Removed practically all references to Library.foldr.
--- a/TFL/post.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/TFL/post.ML Fri Mar 04 15:07:34 2005 +0100
@@ -46,7 +46,7 @@
*--------------------------------------------------------------------------*)
fun termination_goals rules =
map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
- (Library.foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
+ (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
(*---------------------------------------------------------------------------
* Finds the termination conditions in (highly massaged) definition and
--- a/TFL/rules.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/TFL/rules.ML Fri Mar 04 15:07:34 2005 +0100
@@ -133,8 +133,8 @@
fun FILTER_DISCH_ALL P thm =
let fun check tm = P (#t (Thm.rep_cterm tm))
- in Library.foldr (fn (tm,th) => if check tm then DISCH tm th else th)
- (chyps thm, thm)
+ in foldr (fn (tm,th) => if check tm then DISCH tm th else th)
+ thm (chyps thm)
end;
(* freezeT expensive! *)
--- a/TFL/tfl.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/TFL/tfl.ML Fri Mar 04 15:07:34 2005 +0100
@@ -336,7 +336,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 = Library.foldr add_term_names (R,[])
+ val names = foldr add_term_names [] R
val atype = type_of(hd pats)
and aname = variant names "a"
val a = Free(aname,atype)
@@ -499,7 +499,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 (variant (Library.foldr add_term_names (eqns,[])) Rname,
+ val R = Free (variant (foldr 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)
@@ -540,7 +540,7 @@
prths extractants;
())
else ()
- val TCs = Library.foldr (gen_union (op aconv)) (TCl, [])
+ val TCs = 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'
@@ -698,7 +698,7 @@
let val tych = Thry.typecheck thy
val ty_info = Thry.induct_info thy
in fn pats =>
- let val names = Library.foldr add_term_names (pats,[])
+ let val names = foldr add_term_names [] pats
val T = type_of (hd pats)
val aname = Term.variant names "a"
val vname = Term.variant (aname::names) "v"
@@ -851,8 +851,8 @@
val (pats,TCsl) = ListPair.unzip pat_TCs_list
val case_thm = complete_cases thy pats
val domain = (type_of o hd) pats
- val Pname = Term.variant (Library.foldr (Library.foldr add_term_names)
- (pats::TCsl, [])) "P"
+ val Pname = Term.variant (foldr (Library.foldr add_term_names)
+ [] (pats::TCsl)) "P"
val P = Free(Pname, domain --> HOLogic.boolT)
val Sinduct = R.SPEC (tych P) Sinduction
val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
@@ -862,7 +862,7 @@
val cases = map (fn pat => 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 (variant (Library.foldr add_term_names (map concl proved_cases, []))
+ val v = Free (variant (foldr add_term_names [] (map concl proved_cases))
"v",
domain)
val vtyped = tych v
--- a/etc/settings Fri Mar 04 11:44:26 2005 +0100
+++ b/etc/settings Fri Mar 04 15:07:34 2005 +0100
@@ -46,7 +46,7 @@
# Standard ML of New Jersey 110 or later
#ML_SYSTEM=smlnj-110
-#ML_HOME="$ISABELLE_HOME/../smlnj/bin"
+#ML_HOME="/usr/local/smlnj/bin"
#ML_OPTIONS="@SMLdebug=/dev/null"
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
--- a/lib/Tools/convert Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/convert Fri Mar 04 15:07:34 2005 +0100
@@ -36,7 +36,7 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS \( -name \*.ML \) -print | \
xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl"
--- a/lib/Tools/expandshort Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/expandshort Fri Mar 04 15:07:34 2005 +0100
@@ -34,6 +34,6 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/expandshort.pl"
--- a/lib/Tools/fixclasimp Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/fixclasimp Fri Mar 04 15:07:34 2005 +0100
@@ -34,6 +34,6 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixclasimp.pl"
--- a/lib/Tools/fixdatatype Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/fixdatatype Fri Mar 04 15:07:34 2005 +0100
@@ -34,7 +34,7 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdatatype.pl"
--- a/lib/Tools/fixdots Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/fixdots Fri Mar 04 15:07:34 2005 +0100
@@ -34,7 +34,7 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdots.pl"
--- a/lib/Tools/fixgoal Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/fixgoal Fri Mar 04 15:07:34 2005 +0100
@@ -34,6 +34,6 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgoal.pl"
--- a/lib/Tools/fixgreek Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/fixgreek Fri Mar 04 15:07:34 2005 +0100
@@ -35,7 +35,7 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
--- a/lib/Tools/fixseq Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/fixseq Fri Mar 04 15:07:34 2005 +0100
@@ -34,6 +34,6 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixseq.pl"
--- a/lib/Tools/fixsome Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/fixsome Fri Mar 04 15:07:34 2005 +0100
@@ -34,7 +34,7 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixsome.pl"
--- a/lib/Tools/install Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/install Fri Mar 04 15:07:34 2005 +0100
@@ -80,7 +80,7 @@
# standalone binaries
#set by configure
-AUTO_BASH=bash
+AUTO_BASH=/bin/bash
case "$AUTO_BASH" in
/*)
--- a/lib/Tools/logo Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/logo Fri Mar 04 15:07:34 2005 +0100
@@ -71,7 +71,7 @@
fi
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
if [ "$OUTFILE" = "-" ]; then
"$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
--- a/lib/Tools/mkdir Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/mkdir Fri Mar 04 15:07:34 2005 +0100
@@ -198,7 +198,7 @@
# document directory
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
if [ -e document ]; then
echo "keeping $PREFIX/document" >&2
--- a/lib/Tools/unsymbolize Fri Mar 04 11:44:26 2005 +0100
+++ b/lib/Tools/unsymbolize Fri Mar 04 15:07:34 2005 +0100
@@ -35,7 +35,7 @@
## main
#set by configure
-AUTO_PERL=perl
+AUTO_PERL=/usr/bin/perl
find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"
--- a/src/FOLP/simp.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/FOLP/simp.ML Fri Mar 04 15:07:34 2005 +0100
@@ -161,7 +161,7 @@
in case f of
Const(c,T) =>
if c mem ccs
- then Library.foldr add_hvars (args,hvars)
+ then foldr add_hvars hvars args
else add_term_vars(tm,hvars)
| _ => add_term_vars(tm,hvars)
end
@@ -173,7 +173,7 @@
if at then vars else add_term_vars(tm,vars)
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
in if length(tml)=length(al)
- then Library.foldr itf (tml~~al,vars)
+ then foldr itf vars (tml~~al)
else vars
end
fun add_vars (tm,vars) = case tm of
@@ -194,12 +194,12 @@
val lhs = rhs_of_eq 1 thm'
val rhs = lhs_of_eq nops thm'
val asms = tl(rev(tl(prems_of thm')))
- val hvars = Library.foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
+ val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms)
val hvars = add_new_asm_vars new_asms (rhs,hvars)
fun it_asms (asm,hvars) =
if atomic asm then add_new_asm_vars new_asms (asm,hvars)
else add_term_frees(asm,hvars)
- val hvars = Library.foldr it_asms (asms,hvars)
+ val hvars = foldr it_asms hvars asms
val hvs = map (#1 o dest_Var) hvars
val refl1_tac = refl_tac 1
fun norm_step_tac st = st |>
@@ -252,12 +252,12 @@
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
net);
-val insert_thms = Library.foldr insert_thm_warn;
+val insert_thms = foldr insert_thm_warn;
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
let val thms = mk_simps thm
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
- simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net)}
+ simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms}
end;
val op addrews = Library.foldl addrew;
@@ -265,7 +265,7 @@
fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
let val congs' = thms @ congs;
in SS{auto_tac=auto_tac, congs= congs',
- cong_net= insert_thms (map mk_trans thms,cong_net),
+ cong_net= insert_thms cong_net (map mk_trans thms),
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
end;
@@ -278,12 +278,12 @@
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;
net);
-val delete_thms = Library.foldr delete_thm_warn;
+val delete_thms = foldr delete_thm_warn;
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
in SS{auto_tac=auto_tac, congs= congs',
- cong_net= delete_thms(map mk_trans thms,cong_net),
+ cong_net= delete_thms cong_net (map mk_trans thms),
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
end;
@@ -295,7 +295,7 @@
([],simps'))
val (thms,simps') = find(simps,[])
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
- simps = simps', simp_net = delete_thms(thms,simp_net)}
+ simps = simps', simp_net = delete_thms simp_net thms}
end;
val op delrews = Library.foldl delrew;
@@ -439,7 +439,7 @@
val thms = map (trivial o cterm_of(#sign(rep_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' = Library.foldr lhs_insert_thm (rwrls,anet)
+ val anet' = foldr lhs_insert_thm anet rwrls
in if !tracing andalso not(null new_rws)
then (writeln"Adding rewrites:"; prths new_rws; ())
else ();
--- a/src/HOL/Import/proof_kernel.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Import/proof_kernel.ML Fri Mar 04 15:07:34 2005 +0100
@@ -675,7 +675,7 @@
val (c,asl) = case terms of
[] => raise ERR "x2p" "Bad oracle description"
| (hd::tl) => (hd,tl)
- val tg = Library.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) (ors,Tag.empty_tag)
+ val tg = 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
@@ -1064,7 +1064,7 @@
| process _ = raise ERR "disamb_helper" "Internal error"
val (vars',rens',inst) =
- Library.foldr process (varstm,(vars,rens,[]))
+ foldr process (vars,rens,[]) varstm
in
({vars=vars',rens=rens'},inst)
end
@@ -1100,22 +1100,22 @@
end
fun disamb_terms_from info tms =
- Library.foldr (fn (tm,(info,tms)) =>
+ foldr (fn (tm,(info,tms)) =>
let
val (info',tm') = disamb_term_from info tm
in
(info',tm'::tms)
end)
- (tms,(info,[]))
+ (info,[]) tms
fun disamb_thms_from info hthms =
- Library.foldr (fn (hthm,(info,thms)) =>
+ foldr (fn (hthm,(info,thms)) =>
let
val (info',tm') = disamb_thm_from info hthm
in
(info',tm'::thms)
end)
- (hthms,(info,[]))
+ (info,[]) hthms
fun disamb_term tm = disamb_term_from disamb_info_empty tm
fun disamb_terms tms = disamb_terms_from disamb_info_empty tms
@@ -1127,7 +1127,7 @@
let
val vars = collect_vars (prop_of th)
val (rens',inst,_) =
- Library.foldr (fn((ren as (vold as Free(vname,_),vnew)),
+ foldr (fn((ren as (vold as Free(vname,_),vnew)),
(rens,inst,vars)) =>
(case Library.find_first (fn Free(v,_) => v = vname | _ => false) vars of
SOME v' => if v' = vold
@@ -1135,7 +1135,7 @@
else (ren::rens,(vold,vnew)::inst,vnew::vars)
| NONE => (rens,(vnew,vold)::inst,vold::vars))
| _ => raise ERR "norm_hthm" "Internal error")
- (rens,([],[],vars))
+ ([],[],vars) rens
val (dom,rng) = ListPair.unzip inst
val th' = mk_INST (map (cterm_of sg) dom) (map (cterm_of sg) rng) th
val nvars = collect_vars (prop_of th')
@@ -1794,7 +1794,7 @@
| inst_type ty1 ty2 (ty as Type(name,tys)) =
Type(name,map (inst_type ty1 ty2) tys)
in
- Library.foldr (fn (v,th) =>
+ foldr (fn (v,th) =>
let
val cdom = fst (dom_rng (fst (dom_rng cty)))
val vty = type_of v
@@ -1802,11 +1802,11 @@
val cc = cterm_of sg (Const(cname,newcty))
in
mk_COMB (mk_REFL cc) (mk_ABS v th sg) sg
- end) (vlist',th)
+ end) th vlist'
end
| SOME _ => raise ERR "GEN_ABS" "Bad constant"
| NONE =>
- Library.foldr (fn (v,th) => mk_ABS v th sg) (vlist',th)
+ foldr (fn (v,th) => mk_ABS v th sg) th vlist'
val res = HOLThm(rens_of info',th1)
val _ = message "RESULT:"
val _ = if_debug pth res
@@ -1970,8 +1970,8 @@
Theory.add_consts_i consts thy'
end
- val thy1 = Library.foldr (fn(name,thy)=>
- snd (get_defname thyname name thy)) (names,thy1)
+ val thy1 = foldr (fn(name,thy)=>
+ snd (get_defname thyname name thy)) thy1 names
fun new_name name = fst (get_defname thyname name thy1)
val (thy',res) = SpecificationPackage.add_specification_i NONE
(map (fn name => (new_name name,name,false)) names)
@@ -1989,12 +1989,12 @@
then quotename name
else (quotename newname) ^ ": " ^ (quotename name),thy')
end
- val (new_names,thy') = Library.foldr (fn(name,(names,thy)) =>
+ val (new_names,thy') = foldr (fn(name,(names,thy)) =>
let
val (name',thy') = handle_const (name,thy)
in
(name'::names,thy')
- end) (names,([],thy'))
+ end) ([],thy') names
val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
"\n by (import " ^ thyname ^ " " ^ thmname ^ ")")
thy'
--- a/src/HOL/Import/replay.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Import/replay.ML Fri Mar 04 15:07:34 2005 +0100
@@ -25,12 +25,12 @@
end
| rp (PSubst(prfs,ctxt,prf)) thy =
let
- val (thy',ths) = Library.foldr (fn (p,(thy,ths)) =>
+ val (thy',ths) = foldr (fn (p,(thy,ths)) =>
let
val (thy',th) = rp' p thy
in
(thy',th::ths)
- end) (prfs,(thy,[]))
+ end) (thy,[]) prfs
val (thy'',th) = rp' prf thy'
in
P.SUBST ths ctxt th thy''
--- a/src/HOL/Import/shuffler.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Import/shuffler.ML Fri Mar 04 15:07:34 2005 +0100
@@ -553,13 +553,13 @@
end
val collect_ignored =
- Library.foldr (fn (thm,cs) =>
+ foldr (fn (thm,cs) =>
let
val (lhs,rhs) = Logic.dest_equals (prop_of thm)
val ignore_lhs = term_consts lhs \\ term_consts rhs
val ignore_rhs = term_consts rhs \\ term_consts lhs
in
- Library.foldr (op ins_string) (ignore_lhs @ ignore_rhs,cs)
+ foldr (op ins_string) cs (ignore_lhs @ ignore_rhs)
end)
(* set_prop t thms tries to make a theorem with the proposition t from
@@ -570,8 +570,8 @@
let
val sg = sign_of thy
val vars = add_term_frees (t,add_term_vars (t,[]))
- val closed_t = Library.foldr (fn (v,body) => let val vT = type_of v
- in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t)
+ val closed_t = foldr (fn (v,body) => let val vT = type_of v
+ in all vT $ (Abs("x",vT,abstract_over(v,body))) end) t vars
val rew_th = norm_term thy closed_t
val rhs = snd (dest_equals (cprop_of rew_th))
@@ -610,7 +610,7 @@
fun find_potential thy t =
let
val shuffles = ShuffleData.get thy
- val ignored = collect_ignored(shuffles,[])
+ val ignored = collect_ignored [] shuffles
val rel_consts = term_consts t \\ ignored
val pot_thms = PureThy.thms_containing_consts thy rel_consts
in
--- a/src/HOL/Integ/cooper_dec.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Integ/cooper_dec.ML Fri Mar 04 15:07:34 2005 +0100
@@ -442,7 +442,7 @@
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
- |_ => Library.foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
+ |_ => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
end;
@@ -736,7 +736,7 @@
in (rw,HOLogic.mk_disj(F',rf))
end)
val f = if b then linear_add else linear_sub
- val p_elements = Library.foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
+ val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (1 upto d)
in h p_elements
end;
--- a/src/HOL/Integ/presburger.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Integ/presburger.ML Fri Mar 04 15:07:34 2005 +0100
@@ -162,10 +162,10 @@
fun abstract_pres sg fm =
- Library.foldr (fn (t, u) =>
+ foldr (fn (t, u) =>
let val T = fastype_of t
in all T $ Abs ("x", T, abstract_over (t, u)) end)
- (getfuncs fm, fm);
+ fm (getfuncs fm);
@@ -219,11 +219,11 @@
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
val (rhs,irhs) = List.partition (relevant (rev ps)) hs
val np = length ps
- val (fm',np) = Library.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
- (ps,(Library.foldr HOLogic.mk_imp (rhs, c), np))
+ val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
+ (foldr HOLogic.mk_imp c rhs, np) ps
val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
(term_frees fm' @ term_vars fm');
- val fm2 = Library.foldr mk_all2 (vs, fm')
+ val fm2 = foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
(*Object quantifier to meta --*)
--- a/src/HOL/Library/EfficientNat.thy Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Library/EfficientNat.thy Fri Mar 04 15:07:34 2005 +0100
@@ -191,8 +191,8 @@
let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
in
if forall (can (dest o concl_of)) ths andalso
- exists (fn th => "Suc" mem Library.foldr add_term_consts
- (List.mapPartial (try dest) (concl_of th :: prems_of th), [])) ths
+ exists (fn th => "Suc" mem foldr add_term_consts
+ [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) ths
then remove_suc_clause thy ths else ths
end;
--- a/src/HOL/Matrix/eq_codegen.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Matrix/eq_codegen.ML Fri Mar 04 15:07:34 2005 +0100
@@ -377,8 +377,8 @@
| SOME thms => SOME (unsuffix "_case" (Sign.base_name s) ^ ".cases",
map (fn i => Sign.base_name s ^ "_" ^ string_of_int i)
(1 upto length thms) ~~ thms)))
- (Library.foldr add_term_consts (map (prop_of o snd)
- (List.concat (map (#3 o snd) fs')), []));
+ (foldr add_term_consts [] (map (prop_of o snd)
+ (List.concat (map (#3 o snd) fs'))));
val case_vals = map (fn (s, cs) => mk_vall (map fst cs)
[Pretty.str "map my_mk_meta_eq", Pretty.brk 1,
Pretty.str ("(thms \"" ^ s ^ "\")")]) case_thms;
@@ -460,10 +460,10 @@
fun mk_edges (s, _, ths) = map (pair s) (distinct
(List.mapPartial (fn t => Option.map #1 (lookup sg eqns' t))
(List.concat (map (term_consts' o prop_of o snd) ths))));
- val gr = Library.foldr (uncurry Graph.add_edge)
- (map (pair "" o #1) eqns @ List.concat (map mk_edges eqns),
- Library.foldr (uncurry Graph.new_node)
- (("", Bound 0) :: map mk_node eqns, Graph.empty));
+ val gr = foldr (uncurry Graph.add_edge)
+ (Library.foldr (uncurry Graph.new_node)
+ (("", Bound 0) :: map mk_node eqns, Graph.empty))
+ (map (pair "" o #1) eqns @ List.concat (map mk_edges eqns));
val keys = rev (Graph.all_succs gr [""] \ "");
fun gr_ord (x :: _, y :: _) =
int_ord (find_index (equal x) keys, find_index (equal y) keys);
--- a/src/HOL/Modelcheck/mucke_oracle.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Fri Mar 04 15:07:34 2005 +0100
@@ -253,7 +253,7 @@
fun newName (Var(ix,_), (pairs,used)) =
let val v = variant used (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
- val (alist, _) = Library.foldr newName (vars, ([], used));
+ val (alist, _) = foldr newName ([], used) vars;
fun mk_inst (Var(v,T)) =
(Var(v,T),
Free(valOf (assoc(alist,v)), T));
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Fri Mar 04 15:07:34 2005 +0100
@@ -442,7 +442,7 @@
val ts = coeffs_of t
in case ts of
[] => raise DVD_UNKNOWN
- |_ => Library.foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
+ |_ => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
end;
@@ -736,7 +736,7 @@
in (rw,HOLogic.mk_disj(F',rf))
end)
val f = if b then linear_add else linear_sub
- val p_elements = Library.foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
+ val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (1 upto d)
in h p_elements
end;
--- a/src/HOL/Tools/Presburger/presburger.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML Fri Mar 04 15:07:34 2005 +0100
@@ -162,10 +162,10 @@
fun abstract_pres sg fm =
- Library.foldr (fn (t, u) =>
+ foldr (fn (t, u) =>
let val T = fastype_of t
in all T $ Abs ("x", T, abstract_over (t, u)) end)
- (getfuncs fm, fm);
+ fm (getfuncs fm);
@@ -219,11 +219,11 @@
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
val (rhs,irhs) = List.partition (relevant (rev ps)) hs
val np = length ps
- val (fm',np) = Library.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
- (ps,(Library.foldr HOLogic.mk_imp (rhs, c), np))
+ val (fm',np) = foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
+ (foldr HOLogic.mk_imp c rhs, np) ps
val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
(term_frees fm' @ term_vars fm');
- val fm2 = Library.foldr mk_all2 (vs, fm')
+ val fm2 = foldr mk_all2 fm' vs
in (fm2, np + length vs, length rhs) end;
(*Object quantifier to meta --*)
--- a/src/HOL/Tools/datatype_abs_proofs.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Mar 04 15:07:34 2005 +0100
@@ -97,7 +97,7 @@
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
- val used = Library.foldr add_typ_tfree_names (recTs, []);
+ val used = foldr 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)));
@@ -139,7 +139,7 @@
end;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
- val (_, _, prems, t1s, t2s) = Library.foldr mk_prem (cargs ~~ Ts, (1, 1, [], [], []))
+ val (_, _, prems, t1s, t2s) = foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
(HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
@@ -269,7 +269,7 @@
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
- val used = Library.foldr add_typ_tfree_names (recTs, []);
+ val used = foldr add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
val T' = TFree (variant used "'t", HOLogic.typeS);
@@ -401,7 +401,7 @@
val t = if k = 0 then HOLogic.zero else
foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
in
- Library.foldr (fn (T, t') => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT, t)
+ foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
end;
val fs = List.concat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
--- a/src/HOL/Tools/datatype_aux.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Fri Mar 04 15:07:34 2005 +0100
@@ -155,8 +155,8 @@
val prem' = hd (prems_of exhaustion);
val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
- cterm_of sg (Library.foldr (fn ((_, T), t) => Abs ("z", T, t))
- (params, Bound 0)))] exhaustion
+ cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
+ (Bound 0) params))] exhaustion
in compose_tac (false, exhaustion', nprems_of exhaustion) i state
end;
@@ -265,8 +265,8 @@
fun get_branching_types descr sorts =
map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
- Library.foldl (fn (Ts', (_, cargs)) => Library.foldr op union (map (fst o strip_dtyp)
- cargs, Ts')) (Ts, constrs)) ([], descr));
+ Library.foldl (fn (Ts', (_, cargs)) => foldr op union Ts' (map (fst o strip_dtyp)
+ cargs)) (Ts, constrs)) ([], descr));
fun get_arities descr = Library.foldl (fn (is, (_, (_, _, constrs))) =>
Library.foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)
--- a/src/HOL/Tools/datatype_codegen.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Fri Mar 04 15:07:34 2005 +0100
@@ -201,8 +201,8 @@
let
val ts1 = Library.take (i, ts);
val t :: ts2 = Library.drop (i, ts);
- val names = Library.foldr add_term_names (ts1,
- map (fst o fst o dest_Var) (Library.foldr add_term_vars (ts1, [])));
+ val names = foldr add_term_names
+ (map (fst o fst o dest_Var) (foldr 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_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/datatype_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -169,7 +169,7 @@
fun occs_in_prems tacf vars =
SUBGOAL (fn (Bi, i) =>
(if exists (fn Free (a, _) => a mem vars)
- (Library.foldr add_term_frees (#2 (strip_context Bi), []))
+ (foldr add_term_frees [] (#2 (strip_context Bi)))
then warning "Induction variable occurs also among premises!"
else ();
tacf i));
@@ -431,7 +431,7 @@
if length dt <> length vs then
case_error ("Wrong number of arguments for constructor " ^ s)
(SOME tname) vs
- else (cases \ c, Library.foldr abstr (vs, t)))
+ else (cases \ c, foldr abstr t vs))
val (cases'', fs) = foldl_map find_case (cases', constrs)
in case (cases'', length constrs = length cases', default) of
([], true, SOME _) =>
@@ -542,32 +542,32 @@
(********************* axiomatic introduction of datatypes ********************)
fun add_and_get_axioms_atts label tnames attss ts thy =
- Library.foldr (fn (((tname, atts), t), (thy', axs)) =>
+ foldr (fn (((tname, atts), t), (thy', axs)) =>
let
val (thy'', [ax]) = thy' |>
Theory.add_path tname |>
PureThy.add_axioms_i [((label, t), atts)];
in (Theory.parent_path thy'', ax::axs)
- end) (tnames ~~ attss ~~ ts, (thy, []));
+ end) (thy, []) (tnames ~~ attss ~~ ts);
fun add_and_get_axioms label tnames =
add_and_get_axioms_atts label tnames (replicate (length tnames) []);
fun add_and_get_axiomss label tnames tss thy =
- Library.foldr (fn ((tname, ts), (thy', axss)) =>
+ foldr (fn ((tname, ts), (thy', axss)) =>
let
val (thy'', [axs]) = thy' |>
Theory.add_path tname |>
PureThy.add_axiomss_i [((label, ts), [])];
in (Theory.parent_path thy'', axs::axss)
- end) (tnames ~~ tss, (thy, []));
+ end) (thy, []) (tnames ~~ tss);
fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy =
let
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
- val used = Library.foldr add_typ_tfree_names (recTs, []);
+ val used = foldr add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
@@ -694,7 +694,7 @@
Theory.add_path (space_implode "_" new_type_names) |>
add_rules simps case_thms size_thms rec_thms inject distinct
weak_case_congs Simplifier.cong_add_global |>
- put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
+ put_datatypes (foldr Symtab.update dt_info dt_infos) |>
add_cases_induct dt_infos induct |>
Theory.parent_path |>
(#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
@@ -752,7 +752,7 @@
Theory.add_path (space_implode "_" new_type_names) |>
add_rules simps case_thms size_thms rec_thms inject distinct
weak_case_congs (Simplifier.change_global_ss (op addcongs)) |>
- put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
+ put_datatypes (foldr Symtab.update dt_info dt_infos) |>
add_cases_induct dt_infos induct |>
Theory.parent_path |>
(#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
@@ -860,7 +860,7 @@
Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
add_rules simps case_thms size_thms rec_thms inject distinct
weak_case_congs (Simplifier.change_global_ss (op addcongs)) |>
- put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
+ put_datatypes (foldr Symtab.update dt_info dt_infos) |>
add_cases_induct dt_infos induction' |>
Theory.parent_path |>
(#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
@@ -916,7 +916,7 @@
fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
let
val (cargs', sorts'') = Library.foldl (prep_typ sign) (([], sorts'), cargs);
- val _ = (case Library.foldr add_typ_tfree_names (cargs', []) \\ tvs of
+ val _ = (case foldr add_typ_tfree_names [] cargs' \\ tvs of
[] => ()
| vs => error ("Extra type variables on rhs: " ^ commas vs))
in (constrs @ [((if flat_names then Sign.full_name sign else
--- a/src/HOL/Tools/datatype_prop.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/datatype_prop.ML Fri Mar 04 15:07:34 2005 +0100
@@ -80,7 +80,7 @@
(map HOLogic.mk_eq (frees ~~ frees')))))::injs
end;
- in map (fn (d, T) => Library.foldr (make_inj T) (#3 (snd d), []))
+ in map (fn (d, T) => foldr (make_inj T) [] (#3 (snd d)))
((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
end;
@@ -182,7 +182,7 @@
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
- val used = Library.foldr add_typ_tfree_names (recTs, []);
+ val used = foldr add_typ_tfree_names [] recTs;
val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
@@ -232,7 +232,7 @@
let
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
- val used = Library.foldr add_typ_tfree_names (recTs, []);
+ val used = foldr add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
val T' = TFree (variant used "'t", HOLogic.typeS);
@@ -317,7 +317,7 @@
let
val descr' = List.concat descr;
val recTs = get_rec_types descr' sorts;
- val used' = Library.foldr add_typ_tfree_names (recTs, []);
+ val used' = foldr add_typ_tfree_names [] recTs;
val newTs = Library.take (length (hd descr), recTs);
val T' = TFree (variant used' "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
@@ -334,13 +334,13 @@
val eqn = HOLogic.mk_eq (Free ("x", T),
list_comb (Const (cname, Ts ---> T), frees));
val P' = P $ list_comb (f, frees)
- in ((Library.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
- (frees, HOLogic.imp $ eqn $ P'))::t1s,
- (Library.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
- (frees, HOLogic.conj $ eqn $ (HOLogic.Not $ P')))::t2s)
+ in ((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))
+ (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
end;
- val (t1s, t2s) = Library.foldr process_constr (constrs ~~ fs, ([], []));
+ val (t1s, t2s) = foldr process_constr ([], []) (constrs ~~ fs);
val lhs = P $ (comb_t $ Free ("x", T))
in
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
@@ -475,9 +475,9 @@
val tnames = variantlist (make_tnames Ts, ["v"]);
val frees = tnames ~~ Ts
in
- Library.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
- (frees, HOLogic.mk_eq (Free ("v", T),
- list_comb (Const (cname, Ts ---> T), map Free frees)))
+ 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
in map (fn ((_, (_, _, constrs)), T) =>
--- a/src/HOL/Tools/datatype_realizer.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML Fri Mar 04 15:07:34 2005 +0100
@@ -144,8 +144,8 @@
tname_of (body_type T) mem ["set", "bool"]) ivs);
val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
- val prf = Library.foldr forall_intr_prf (ivs2,
- Library.foldr (fn ((f, p), prf) =>
+ val prf = foldr forall_intr_prf
+ (foldr (fn ((f, p), prf) =>
(case head_of (strip_abs_body f) of
Free (s, T) =>
let val T' = Type.varifyT T
@@ -153,12 +153,12 @@
(Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
end
| _ => AbsP ("H", SOME p, prf)))
- (rec_fns ~~ prems_of thm, Proofterm.proof_combP
- (prf_of thm', map PBound (length prems - 1 downto 0))));
+ (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 (Library.foldr (uncurry lambda)
- (map Logic.unvarify ivs1 @ filter_out is_unit
- (map (head_of o strip_abs_body) rec_fns), r));
+ val r' = if null is then r else Logic.varify (foldr (uncurry lambda)
+ r (map Logic.unvarify ivs1 @ filter_out is_unit
+ (map (head_of o strip_abs_body) rec_fns)));
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
@@ -209,10 +209,10 @@
val P = Var (("P", 0), rT' --> HOLogic.boolT);
val prf = forall_intr_prf (y, forall_intr_prf (P,
- Library.foldr (fn ((p, r), prf) =>
+ foldr (fn ((p, r), prf) =>
forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
- prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm',
- map PBound (length prems - 1 downto 0)))));
+ prf))) (Proofterm.proof_combP (prf_of thm',
+ map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
val r' = Logic.varify (Abs ("y", Type.varifyT T,
list_abs (map dest_Free rs, list_comb (r,
map Bound ((length rs - 1 downto 0) @ [length rs])))));
--- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Mar 04 15:07:34 2005 +0100
@@ -78,7 +78,7 @@
val branchT = if null branchTs then HOLogic.unitT
else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
val arities = get_arities descr' \ 0;
- val unneeded_vars = hd tyvars \\ Library.foldr add_typ_tfree_names (leafTs' @ branchTs, []);
+ val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
val recTs = get_rec_types descr' sorts;
val newTs = Library.take (length (hd descr), recTs);
@@ -134,7 +134,7 @@
in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
end;
- val mk_lim = Library.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
+ val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
(************** generate introduction rules for representing set **********)
@@ -153,14 +153,14 @@
in (j + 1, list_all (map (pair "x") Ts,
HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
Const (List.nth (rep_set_names, k), UnivT)))) :: prems,
- mk_lim (Ts, free_t) :: ts)
+ mk_lim free_t Ts :: ts)
end
| _ =>
let val T = typ_of_dtyp descr' sorts dt
in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
end);
- val (_, prems, ts) = Library.foldr mk_prem (cargs, (1, [], []));
+ val (_, prems, ts) = foldr mk_prem (1, [], []) cargs;
val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
(mk_univ_inj ts n i, Const (s, UnivT)))
in Logic.list_implies (prems, concl)
@@ -210,13 +210,13 @@
let val T = typ_of_dtyp descr' sorts dt;
val free_t = mk_Free "x" T j
in (case (strip_dtyp dt, strip_type T) of
- ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us,
- Const (List.nth (all_rep_names, m), U --> Univ_elT) $
- app_bnds free_t (length Us)) :: r_args)
+ ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
+ (Const (List.nth (all_rep_names, m), U --> Univ_elT) $
+ app_bnds free_t (length Us)) Us :: r_args)
| _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
end;
- val (_, l_args, r_args) = Library.foldr constr_arg (cargs, (1, [], []));
+ val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
@@ -329,13 +329,13 @@
val (Us, U) = strip_type T'
in (case strip_dtyp dt of
(_, DtRec j) => if j mem ks' then
- (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds
- (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))],
+ (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
+ (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
Ts @ [Us ---> Univ_elT])
else
- (i2 + 1, i2', ts @ [mk_lim (Us,
- Const (List.nth (all_rep_names, j), U --> Univ_elT) $
- app_bnds (mk_Free "x" T' i2) (length Us))], Ts)
+ (i2 + 1, i2', ts @ [mk_lim
+ (Const (List.nth (all_rep_names, j), U --> Univ_elT) $
+ app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
| _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
end;
@@ -380,8 +380,8 @@
in (thy', char_thms' @ char_thms) end;
- val (thy5, iso_char_thms) = Library.foldr make_iso_defs
- (tl descr, (add_path flat_names big_name thy4, []));
+ val (thy5, iso_char_thms) = foldr make_iso_defs
+ (add_path flat_names big_name thy4, []) (tl descr);
(* prove isomorphism properties *)
@@ -469,8 +469,8 @@
in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
end;
- val (iso_inj_thms_unfolded, iso_elem_thms) = Library.foldr prove_iso_thms
- (tl descr, ([], map #3 newT_iso_axms));
+ val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
+ ([], map #3 newT_iso_axms) (tl descr);
val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded;
(* prove x : dt_rep_set_i --> x : range dt_Rep_i *)
--- a/src/HOL/Tools/inductive_codegen.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Mar 04 15:07:34 2005 +0100
@@ -49,12 +49,12 @@
in (case concl_of thm of
_ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
Const (s, _) =>
- let val cs = Library.foldr add_term_consts (prems_of thm, [])
+ let val cs = foldr add_term_consts [] (prems_of thm)
in (CodegenData.put
{intros = Symtab.update ((s,
getOpt (Symtab.lookup (intros, s), []) @ [thm]), intros),
- graph = Library.foldr (uncurry (Graph.add_edge o pair s))
- (cs, Library.foldl add_node (graph, s :: cs)),
+ graph = foldr (uncurry (Graph.add_edge o pair s))
+ (Library.foldl add_node (graph, s :: cs)) cs,
eqns = eqns} thy, thm)
end
| _ => (warn thm; p))
@@ -190,7 +190,7 @@
fun cprod ([], ys) = []
| cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
-fun cprods xss = Library.foldr (map op :: o cprod) (xss, [[]]);
+fun cprods xss = foldr (map op :: o cprod) [[]] xss;
datatype mode = Mode of (int list option list * int list) * mode option list;
@@ -526,7 +526,7 @@
NONE => gr
| SOME (names, intrs) =>
mk_ind_def thy gr dep names [] [] (prep_intrs intrs)))
- (gr, Library.foldr add_term_consts (ts, []))
+ (gr, foldr add_term_consts [] ts)
and mk_ind_def thy gr dep names modecs factorcs intrs =
let val ids = map (mk_const_id (sign_of thy)) names
--- a/src/HOL/Tools/inductive_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -183,8 +183,8 @@
fun varify (t, (i, ts)) =
let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
in (maxidx_of_term t', t'::ts) end;
- val (i, cs') = Library.foldr varify (cs, (~1, []));
- val (i', intr_ts') = Library.foldr varify (intr_ts, (i, []));
+ val (i, cs') = foldr varify (~1, []) cs;
+ val (i', intr_ts') = foldr varify (i, []) intr_ts;
val rec_consts = Library.foldl add_term_consts_2 ([], cs');
val intr_consts = Library.foldl add_term_consts_2 ([], intr_ts');
fun unify (env, (cname, cT)) =
@@ -271,12 +271,12 @@
val remove_split = rewrite_rule [split_conv RS eq_reflection];
-fun split_rule_vars vs rl = standard (remove_split (Library.foldr split_rule_var'
- (mg_prod_factors vs ([], Thm.prop_of rl), rl)));
+fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
+ rl (mg_prod_factors vs ([], Thm.prop_of rl))));
-fun split_rule vs rl = standard (remove_split (Library.foldr split_rule_var'
- (List.mapPartial (fn (t as Var ((a, _), _)) =>
- Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)), rl)));
+fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
+ rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
+ Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)))));
(** process rules **)
@@ -337,7 +337,7 @@
fun mk_elims cs cTs params intr_ts intr_names =
let
- val used = Library.foldr add_term_names (intr_ts, []);
+ val used = foldr add_term_names [] intr_ts;
val [aname, pname] = variantlist (["a", "P"], used);
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
@@ -353,7 +353,7 @@
val a = Free (aname, T);
fun mk_elim_prem (_, t, ts) =
- list_all_free (map dest_Free ((Library.foldr add_term_frees (t::ts, [])) \\ params),
+ list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params),
Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
val c_intrs = (List.filter (equal c o #1 o #1) intrs);
in
@@ -369,7 +369,7 @@
fun mk_indrule cs cTs params intr_ts =
let
- val used = Library.foldr add_term_names (intr_ts, []);
+ val used = foldr add_term_names [] intr_ts;
(* predicates for induction rule *)
@@ -407,8 +407,8 @@
HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
in list_all_free (frees,
- Logic.list_implies (map HOLogic.mk_Trueprop (Library.foldr mk_prem
- (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
+ Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
+ [] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))),
HOLogic.mk_Trueprop (valOf (pred_of u) $ t)))
end;
@@ -422,15 +422,15 @@
let val T = HOLogic.dest_setT (fastype_of c);
val ps = getOpt (assoc (factors, P), []);
val Ts = prodT_factors [] ps T;
- val (frees, x') = Library.foldr (fn (T', (fs, s)) =>
- ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
+ val (frees, x') = foldr (fn (T', (fs, s)) =>
+ ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
val tuple = mk_tuple [] ps T frees;
in ((HOLogic.mk_binop "op -->"
(HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
end;
val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
- (fst (Library.foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
+ (fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds))))
in (preds, ind_prems, mutual_ind_concl,
map (apfst (fst o dest_Free)) factors)
@@ -707,7 +707,7 @@
val fp_name = if coind then gfp_name else lfp_name;
- val used = Library.foldr add_term_names (intr_ts, []);
+ val used = foldr add_term_names [] intr_ts;
val [sname, xname] = variantlist (["S", "x"], used);
(* transform an introduction rule into a conjunction *)
@@ -723,11 +723,11 @@
val Const ("op :", _) $ t $ u =
HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
- in Library.foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
- (frees, foldr1 HOLogic.mk_conj
+ in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
+ (foldr1 HOLogic.mk_conj
(((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
(map (subst o HOLogic.dest_Trueprop)
- (Logic.strip_imp_prems r))))
+ (Logic.strip_imp_prems r)))) frees
end
(* make a disjunction of all introduction rules *)
--- a/src/HOL/Tools/inductive_realizer.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Mar 04 15:07:34 2005 +0100
@@ -41,11 +41,11 @@
| strip _ t = t;
in strip (add_term_free_names (t, [])) t end;
-fun relevant_vars prop = Library.foldr (fn
+fun relevant_vars prop = foldr (fn
(Var ((a, i), T), vs) => (case strip_type T of
(_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
| _ => vs)
- | (_, vs) => vs) (term_vars prop, []);
+ | (_, vs) => vs) [] (term_vars prop);
fun params_of intr = map (fst o fst o dest_Var) (term_vars
(snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
@@ -265,9 +265,9 @@
in (Thm.name_of_thm rule, (vs,
if rt = Extraction.nullt then rt else
- Library.foldr (uncurry lambda) (vs1, rt),
- Library.foldr forall_intr_prf (vs2, mk_prf rs prems (Proofterm.proof_combP
- (prf_of rrule, map PBound (length prems - 1 downto 0))))))
+ foldr (uncurry lambda) rt vs1,
+ foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
+ (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
end;
fun add_rule (rss, r) =
--- a/src/HOL/Tools/meson.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/meson.ML Fri Mar 04 15:07:34 2005 +0100
@@ -188,7 +188,7 @@
let fun name1 (th, (k,ths)) =
(k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
- in fn ths => #2 (Library.foldr name1 (ths, (length ths, []))) end;
+ in fn ths => #2 (foldr name1 (length ths, []) ths) end;
(*Find an all-negative support clause*)
fun is_negative th = forall (not o #1) (literals (prop_of th));
@@ -239,7 +239,7 @@
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
local fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
in
-fun size_of_subgoals st = Library.foldr addconcl (prems_of st, 0)
+fun size_of_subgoals st = foldr addconcl 0 (prems_of st)
end;
(*Negation Normal Form*)
@@ -265,12 +265,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 (map (generalize o nodups) (Library.foldr cnf (ths,[])));
+ sort_clauses (map (generalize o nodups) (foldr cnf [] ths));
(*Convert a list of clauses to (contrapositive) Horn clauses*)
fun make_horns ths =
name_thms "Horn#"
- (gen_distinct Drule.eq_thm_prop (Library.foldr (add_contras clause_rules) (ths,[])));
+ (gen_distinct Drule.eq_thm_prop (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/primrec_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/primrec_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -161,8 +161,8 @@
else
let
val (_, _, eqns) = valOf (assoc (rec_eqns, fname));
- val (fnames', fnss', fns) = Library.foldr (trans eqns)
- (constrs, ((i, fname)::fnames, fnss, []))
+ val (fnames', fnss', fns) = foldr (trans eqns)
+ ((i, fname)::fnames, fnss, []) constrs
in
(fnames', (i, (fname, #1 (snd (hd eqns)), fns))::fnss')
end
@@ -192,10 +192,10 @@
fun make_def sign fs (fname, ls, rec_name, tname) =
let
- val rhs = Library.foldr (fn (T, t) => Abs ("", T, t))
- ((map snd ls) @ [dummyT],
- list_comb (Const (rec_name, dummyT),
- fs @ map Bound (0 ::(length ls downto 1))));
+ val rhs = foldr (fn (T, t) => Abs ("", T, t))
+ (list_comb (Const (rec_name, dummyT),
+ fs @ map Bound (0 ::(length ls downto 1))))
+ ((map snd ls) @ [dummyT]);
val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
Logic.mk_equals (Const (fname, dummyT), rhs))
in Theory.inferT_axm sign defpair end;
@@ -228,7 +228,7 @@
val (eqns, atts) = split_list eqns_atts;
val sg = Theory.sign_of thy;
val dt_info = DatatypePackage.get_datatypes thy;
- val rec_eqns = Library.foldr (process_eqn sg) (map snd eqns, []);
+ val rec_eqns = foldr (process_eqn sg) [] (map snd eqns);
val tnames = distinct (map (#1 o snd) rec_eqns);
val dts = find_dts dt_info tnames tnames;
val main_fns =
@@ -241,9 +241,9 @@
primrec_err ("datatypes " ^ commas_quote tnames ^
"\nare not mutually recursive")
else snd (hd dts);
- val (fnames, fnss) = Library.foldr (process_fun sg descr rec_eqns)
- (main_fns, ([], []));
- val (fs, defs) = Library.foldr (get_fns fnss) (descr ~~ rec_names, ([], []));
+ val (fnames, fnss) = foldr (process_fun sg descr rec_eqns)
+ ([], []) main_fns;
+ val (fs, defs) = foldr (get_fns fnss) ([], []) (descr ~~ rec_names);
val defs' = map (make_def sg fs) defs;
val names1 = map snd fnames;
val names2 = map fst rec_eqns;
--- a/src/HOL/Tools/recdef_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/recdef_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -91,7 +91,7 @@
val (del, rest) = Library.partition (Library.equal c o fst) congs;
in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
-val add_congs = curry (Library.foldr (uncurry add_cong));
+val add_congs = foldr (uncurry add_cong);
end;
@@ -272,7 +272,7 @@
fun prepare_hints_old thy (ss, thms) =
let val {simps, congs, wfs} = get_global_hints thy
- in (Classical.claset_of thy, ss addsimps simps, map #2 (add_congs thms congs), wfs) end;
+ in (Classical.claset_of thy, ss addsimps simps, map #2 (add_congs congs thms), wfs) end;
val add_recdef_old = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints_old false;
--- a/src/HOL/Tools/recfun_codegen.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Fri Mar 04 15:07:34 2005 +0100
@@ -128,9 +128,9 @@
(List.concat (map (get_equations thy) cs));
val (gr3, fundef') = mk_fundef "" "fun "
(Graph.add_edge (dname, dep)
- (Library.foldr (uncurry Graph.new_node) (map (fn k =>
- (k, (SOME (EQN ("", dummyT, dname)), ""))) xs,
- Graph.del_nodes xs gr2))) eqs''
+ (foldr (uncurry Graph.new_node) (Graph.del_nodes xs gr2)
+ (map (fn k =>
+ (k, (SOME (EQN ("", dummyT, dname)), ""))) xs))) eqs''
in put_code fundef' gr3 end
else gr2)
end
--- a/src/HOL/Tools/record_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/record_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -430,7 +430,7 @@
val tsig = Sign.tsig_of sg;
fun unify (t,env) = Type.unify tsig env t;
- val (subst,_) = Library.foldr unify (but_last args ~~ but_last Ts,(Vartab.empty,0));
+ val (subst,_) = foldr unify (Vartab.empty,0) (but_last args ~~ but_last Ts);
val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
in (flds',(more,moreT)) end;
@@ -504,7 +504,7 @@
fun record_update_tr [t, u] =
- Library.foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
+ foldr (op $) t (rev (gen_fields_tr "_updates" "_update" updateN u))
| record_update_tr ts = raise TERM ("record_update_tr", ts);
fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
@@ -584,7 +584,7 @@
val (args,rest) = splitargs (map fst flds') fargs;
val vartypes = map Type.varifyT types;
val argtypes = map to_type args;
- val (subst,_) = Library.foldr unify (vartypes ~~ argtypes,(Vartab.empty,0));
+ val (subst,_) = foldr unify (Vartab.empty,0) (vartypes ~~ argtypes);
val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o
(Envir.norm_type subst) o Type.varifyT)
(but_last alphas);
@@ -777,7 +777,7 @@
::map (apfst NameSpace.base) fs;
val (args',more) = split_last args;
val alphavars = map Type.varifyT (but_last alphas);
- val (subst,_)= Library.foldr unify (alphavars~~args',(Vartab.empty,0));
+ val (subst,_)= foldr unify (Vartab.empty,0) (alphavars~~args');
val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT)))
flds';
in flds''@field_lst more end
@@ -1332,8 +1332,8 @@
val ext_decl = (mk_extC (name,extT) fields_moreTs);
(*
val ext_spec = Const ext_decl :==
- (Library.foldr (uncurry lambda)
- (vars@[more],(mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more])))))
+ (foldr (uncurry lambda)
+ (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more]))
*)
val ext_spec = list_comb (Const ext_decl,vars@[more]) :==
(mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more])));
@@ -1551,7 +1551,7 @@
* of parent extensions, starting with the root of the record hierarchy
*)
fun mk_recordT extT parent_exts =
- Library.foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) (parent_exts,extT);
+ foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) extT parent_exts;
@@ -1605,7 +1605,7 @@
val names = map fst fields;
val extN = full bname;
val types = map snd fields;
- val alphas_fields = Library.foldr add_typ_tfree_names (types,[]);
+ val alphas_fields = foldr add_typ_tfree_names [] types;
val alphas_ext = alphas inter alphas_fields;
val len = length fields;
val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::wN::parent_variants);
@@ -1663,7 +1663,7 @@
let val (args',more) = chop_last args;
fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
fun build Ts =
- Library.foldr mk_ext' (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')),more)
+ 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))
@@ -1822,13 +1822,13 @@
end;
val split_object_prop =
- let fun ALL vs t = Library.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) (vs,t)
+ let fun ALL vs t = 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 = Library.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) (vs,t)
+ let fun EX vs t = 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;
@@ -2048,7 +2048,7 @@
val init_env =
(case parent of
NONE => []
- | SOME (types, _) => Library.foldr Term.add_typ_tfrees (types, []));
+ | SOME (types, _) => foldr Term.add_typ_tfrees [] types);
(* fields *)
--- a/src/HOL/Tools/refute.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/refute.ML Fri Mar 04 15:07:34 2005 +0100
@@ -788,14 +788,14 @@
else
acc)
(* collect argument types *)
- val acc_args = Library.foldr collect_types (Ts, acc')
+ val acc_args = foldr collect_types acc' Ts
(* collect constructor types *)
- val acc_constrs = Library.foldr collect_types (List.concat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args)
+ val acc_constrs = foldr collect_types acc_args (List.concat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs))
in
acc_constrs
end
| NONE => (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
- T ins (Library.foldr collect_types (Ts, acc)))
+ T ins (foldr collect_types acc Ts))
| TFree _ => T ins acc
| TVar _ => T ins acc)
in
@@ -1297,8 +1297,8 @@
let
val Ts = binder_types (fastype_of t)
in
- Library.foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
- (Library.take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
+ foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
+ (list_comb (t, map Bound (i-1 downto 0))) (Library.take (i, Ts))
end;
(* ------------------------------------------------------------------------- *)
@@ -2234,7 +2234,7 @@
val HOLogic_empty_set = Const ("{}", HOLogic_setT)
val HOLogic_insert = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
in
- SOME (Library.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
+ SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) HOLogic_empty_set pairs)
end
| Type ("prop", []) =>
(case index_from_interpretation intr of
--- a/src/HOL/Tools/specification_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/specification_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -141,7 +141,7 @@
val tsig = Sign.tsig_of (sign_of thy)
val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
"Specificaton: Only free variables of sort 'type' allowed"
- val prop_closed = Library.foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop)
+ val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
in
(prop_closed,frees)
end
@@ -182,7 +182,7 @@
in
HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
end
- val ex_prop = Library.foldr mk_exist (proc_consts,prop)
+ val ex_prop = 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/HOL/Tools/split_rule.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/split_rule.ML Fri Mar 04 15:07:34 2005 +0100
@@ -103,14 +103,14 @@
(*curries ALL function variables occurring in a rule's conclusion*)
fun split_rule rl =
- Library.foldr split_rule_var' (Term.term_vars (concl_of rl), rl)
+ foldr split_rule_var' rl (Term.term_vars (concl_of rl))
|> remove_internal_split
|> Drule.standard;
fun complete_split_rule rl =
- fst (Library.foldr complete_split_rule_var
- (collect_vars ([], concl_of rl),
- (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))))
+ fst (foldr complete_split_rule_var
+ (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))
+ (collect_vars ([], concl_of rl)))
|> remove_internal_split
|> Drule.standard
|> RuleCases.save rl;
--- a/src/HOL/ex/svc_funcs.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/ex/svc_funcs.ML Fri Mar 04 15:07:34 2005 +0100
@@ -243,7 +243,7 @@
val body_e = mt pos body (*evaluate now to assign into !nat_vars*)
in
- Library.foldr add_nat_var (!nat_vars, body_e)
+ foldr add_nat_var body_e (!nat_vars)
end;
--- a/src/HOL/hologic.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/hologic.ML Fri Mar 04 15:07:34 2005 +0100
@@ -148,7 +148,7 @@
fun all_const T = Const ("All", [T --> boolT] ---> boolT);
fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
-val list_all = Library.foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P));
+fun list_all (vs,x) = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) x vs;
fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
@@ -246,13 +246,13 @@
local (*currently unused*)
-fun mk_tupleT Ts = Library.foldr mk_prodT (Ts, unitT);
+fun mk_tupleT Ts = foldr mk_prodT unitT Ts;
fun dest_tupleT (Type ("Product_Type.unit", [])) = []
| dest_tupleT (Type ("*", [T, U])) = T :: dest_tupleT U
| dest_tupleT T = raise TYPE ("dest_tupleT", [T], []);
-fun mk_tuple ts = Library.foldr mk_prod (ts, unit);
+fun mk_tuple ts = foldr mk_prod unit ts;
fun dest_tuple (Const ("Product_Type.Unity", _)) = []
| dest_tuple (Const ("Pair", _) $ t $ u) = t :: dest_tuple u
--- a/src/HOLCF/domain/axioms.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOLCF/domain/axioms.ML Fri Mar 04 15:07:34 2005 +0100
@@ -31,8 +31,8 @@
val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %:x_name'));
val when_def = ("when_def",%%:(dname^"_when") ==
- Library.foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
- Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
+ foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
+ Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
fun con_def outer recu m n (_,args) = let
fun idxs z x arg = (if is_lazy arg then fn t => %%:"up"`t else Id)
@@ -43,7 +43,7 @@
fun inj y 1 _ = y
| inj y _ 0 = %%:"sinl"`y
| inj y i j = %%:"sinr"`(inj y (i-1) (j-1));
- in Library.foldr /\# (args, outer (inj (parms args) m n)) end;
+ in foldr /\# (outer (inj (parms args) m n)) args end;
val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo
Library.foldl (op `) (%%:(dname^"_when") ,
@@ -57,15 +57,15 @@
val dis_defs = let
fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) ==
mk_cRep_CFun(%%:(dname^"_when"),map
- (fn (con',args) => (Library.foldr /\#
- (args,if con'=con then %%:"TT" else %%:"FF"))) cons))
+ (fn (con',args) => (foldr /\#
+ (if con'=con then %%:"TT" else %%:"FF") args)) cons))
in map ddef cons end;
val sel_defs = let
fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) ==
mk_cRep_CFun(%%:(dname^"_when"),map
(fn (con',args) => if con'<>con then %%:"UU" else
- Library.foldr /\# (args,Bound (length args - n))) cons));
+ foldr /\# (Bound (length args - n)) args) cons));
in List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
@@ -114,11 +114,12 @@
(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 = Library.foldr mk_conj (mapn rel_app 1 rec_args, mk_conj(
+ val capps = foldr mk_conj (mk_conj(
Bound(allargs_cnt+1)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns1),
- Bound(allargs_cnt+0)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns2)));
- in Library.foldr mk_ex (allvns, Library.foldr mk_conj
- (map (defined o Bound) nonlazy_idxs,capps)) end;
+ Bound(allargs_cnt+0)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns2)))
+ (mapn rel_app 1 rec_args);
+ in 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,
foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
--- a/src/HOLCF/domain/library.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOLCF/domain/library.ML Fri Mar 04 15:07:34 2005 +0100
@@ -18,8 +18,8 @@
| itr (a::l) = f(a, itr l)
in itr l end;
fun foldr' f l = foldr'' f (l,Id);
-fun map_cumulr f start xs = Library.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
- (y::ys,res2)) (xs,([],start));
+fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
+ (y::ys,res2)) ([],start) xs;
fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x;
--- a/src/HOLCF/domain/syntax.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOLCF/domain/syntax.ML Fri Mar 04 15:07:34 2005 +0100
@@ -22,15 +22,14 @@
else foldr' 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) = Library.foldr (op ->>) (map third args,freetvar "t");
+ fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
in
val dtype = Type(dname,typevars);
val dtype2 = foldr' 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",Library.foldr (op ->>) ((map when_type cons'),
- dtype ->> freetvar "t"), NoSyn);
+ val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
val const_copy = (dnam^"_copy", dtypeprod ->> dtype ->> dtype , NoSyn);
end;
@@ -42,7 +41,7 @@
else c::esc cs
| esc [] = []
in implode o esc o Symbol.explode end;
- fun con (name,s,args) = (name,Library.foldr (op ->>) (map third args,dtype),s);
+ fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s);
fun dis (con ,s,_ ) = (dis_name_ con, dtype->>trT,
Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
(* stricly speaking, these constants have one argument,
--- a/src/Provers/blast.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Provers/blast.ML Fri Mar 04 15:07:34 2005 +0100
@@ -751,8 +751,8 @@
end
(*substitute throughout "stack frame"; extract affected formulae*)
fun subFrame ((Gs,Hs), (changed, frames)) =
- let val (changed', Gs') = Library.foldr subForm (Gs, (changed, []))
- val (changed'', Hs') = Library.foldr subForm (Hs, (changed', []))
+ let val (changed', Gs') = foldr subForm (changed, []) Gs
+ val (changed'', Hs') = foldr subForm (changed', []) Hs
in (changed'', (Gs',Hs')::frames) end
(*substitute throughout literals; extract affected ones*)
fun subLit (lit, (changed, nlits)) =
@@ -760,8 +760,8 @@
in if nlit aconv lit then (changed, nlit::nlits)
else ((nlit,true)::changed, nlits)
end
- val (changed, lits') = Library.foldr subLit (lits, ([], []))
- val (changed', pairs') = Library.foldr subFrame (pairs, (changed, []))
+ val (changed, lits') = foldr subLit ([], []) lits
+ val (changed', pairs') = foldr subFrame (changed, []) pairs
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^
" for " ^ traceTerm sign t ^ " in branch" )
else ();
@@ -974,7 +974,7 @@
then lim - (1+log(length rules))
else lim (*discourage branching updates*)
val vars = vars_in_vars vars
- val vars' = Library.foldr add_terms_vars (prems, vars)
+ val vars' = foldr add_terms_vars vars prems
val choices' = (ntrl, nbrs, PRV) :: choices
val tacs' = (tac(updated,false,true))
:: tacs (*no duplication; rotate*)
@@ -1101,7 +1101,7 @@
then
let val updated = ntrl < !ntrail (*branch updated*)
val vars = vars_in_vars vars
- val vars' = Library.foldr add_terms_vars (prems, vars)
+ val vars' = 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/classical.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Provers/classical.ML Fri Mar 04 15:07:34 2005 +0100
@@ -214,7 +214,7 @@
let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
in assume_tac ORELSE'
contr_tac ORELSE'
- biresolve_tac (Library.foldr addrl (rls,[]))
+ biresolve_tac (foldr addrl [] rls)
end;
(*Duplication of hazardous rules, for complete provers*)
@@ -286,7 +286,7 @@
fun rep_cs (CS args) = args;
local
- fun wrap l tac = Library.foldr (fn ((name,tacf),w) => tacf w) (l, tac);
+ fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l;
in
fun appSWrappers (CS{swrappers,...}) = wrap swrappers;
fun appWrappers (CS{uwrappers,...}) = wrap uwrappers;
@@ -316,7 +316,7 @@
fun tag_brls' _ _ [] = []
| tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
-fun insert_tagged_list kbrls netpr = Library.foldr Tactic.insert_tagged_brl (kbrls, netpr);
+fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
(*Insert into netpair that already has nI intr rules and nE elim rules.
Count the intr rules double (to account for swapify). Negate to give the
@@ -324,7 +324,7 @@
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
-fun delete_tagged_list brls netpr = Library.foldr Tactic.delete_tagged_brl (brls, netpr);
+fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
fun delete x = delete_tagged_list (joinrules x);
fun delete' x = delete_tagged_list (joinrules' x);
--- a/src/Provers/induct_method.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Provers/induct_method.ML Fri Mar 04 15:07:34 2005 +0100
@@ -268,8 +268,8 @@
| rename _ thm = thm;
fun find_inductT ctxt insts =
- Library.foldr multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
- |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
+ foldr multiply [[]] (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
+ |> map (InductAttrib.find_inductT ctxt o fastype_of))
|> map join_rules |> List.concat |> map (rename insts);
fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
--- a/src/Provers/order.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Provers/order.ML Fri Mar 04 15:07:34 2005 +0100
@@ -437,7 +437,7 @@
(* Compute, for each adjacency list, the list with reversed edges,
and concatenate these lists. *)
- val flipped = Library.foldr (op @) ((map flip g),nil)
+ val flipped = foldr (op @) nil (map flip g)
in assemble g flipped end
@@ -475,9 +475,9 @@
let
val _ = visited := u :: !visited
val descendents =
- Library.foldr (fn ((v,l),ds) => if been_visited v then ds
+ foldr (fn ((v,l),ds) => if been_visited v then ds
else v :: dfs_visit g v @ ds)
- ((adjacent (op aconv) g u) ,nil)
+ nil (adjacent (op aconv) g u)
in
finish := u :: !finish;
descendents
@@ -525,9 +525,9 @@
let
val _ = visited := u :: !visited
val descendents =
- Library.foldr (fn ((v,l),ds) => if been_visited v then ds
+ foldr (fn ((v,l),ds) => if been_visited v then ds
else v :: dfs_visit g v @ ds)
- ( ((adjacent (op =) g u)) ,nil)
+ nil (adjacent (op =) g u)
in descendents end
in u :: dfs_visit g u end;
--- a/src/Provers/simp.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Provers/simp.ML Fri Mar 04 15:07:34 2005 +0100
@@ -155,7 +155,7 @@
in case f of
Const(c,T) =>
if c mem ccs
- then Library.foldr add_hvars (args,hvars)
+ then foldr add_hvars hvars args
else add_term_vars(tm,hvars)
| _ => add_term_vars(tm,hvars)
end
@@ -167,7 +167,7 @@
if at then vars else add_term_vars(tm,vars)
fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
in if length(tml)=length(al)
- then Library.foldr itf (tml~~al,vars)
+ then foldr itf vars (tml~~al)
else vars
end
fun add_vars (tm,vars) = case tm of
@@ -188,12 +188,12 @@
val lhs = rhs_of_eq 1 thm'
val rhs = lhs_of_eq nops thm'
val asms = tl(rev(tl(prems_of thm')))
- val hvars = Library.foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
+ val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms)
val hvars = add_new_asm_vars new_asms (rhs,hvars)
fun it_asms (asm,hvars) =
if atomic asm then add_new_asm_vars new_asms (asm,hvars)
else add_term_frees(asm,hvars)
- val hvars = Library.foldr it_asms (asms,hvars)
+ val hvars = foldr it_asms hvars asms
val hvs = map (#1 o dest_Var) hvars
val refl1_tac = refl_tac 1
fun norm_step_tac st = st |>
@@ -249,13 +249,13 @@
(writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
net);
-val insert_thms = Library.foldr insert_thm_warn;
+val insert_thms = foldr insert_thm_warn;
fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
splits,split_consts}, thm) =
let val thms = mk_simps thm
in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
- simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net),
+ simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms,
splits=splits,split_consts=split_consts}
end;
@@ -265,7 +265,7 @@
splits,split_consts}, thms) =
let val congs' = thms @ congs;
in SS{auto_tac=auto_tac, congs= congs',
- cong_net= insert_thms (map mk_trans thms,cong_net),
+ cong_net= insert_thms cong_net (map mk_trans thms),
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
splits=splits,split_consts=split_consts}
end;
@@ -294,13 +294,13 @@
(writeln"\nNo such rewrite or congruence rule:"; print_thm th;
net);
-val delete_thms = Library.foldr delete_thm_warn;
+val delete_thms = foldr delete_thm_warn;
fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
splits,split_consts}, thms) =
let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
in SS{auto_tac=auto_tac, congs= congs',
- cong_net= delete_thms(map mk_trans thms,cong_net),
+ cong_net= delete_thms cong_net (map mk_trans thms),
mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
splits=splits,split_consts=split_consts}
end;
@@ -314,7 +314,7 @@
([],simps'))
val (thms,simps') = find(simps,[])
in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
- simps = simps', simp_net = delete_thms(thms,simp_net),
+ simps = simps', simp_net = delete_thms simp_net thms,
splits=splits,split_consts=split_consts}
end;
@@ -460,7 +460,7 @@
val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
val new_rws = flat(map mk_rew_rules thms);
val rwrls = map mk_trans (flat(map mk_rew_rules thms));
- val anet' = Library.foldr lhs_insert_thm (rwrls,anet)
+ val anet' = foldr lhs_insert_thm anet rwrls
in if !tracing andalso not(null new_rws)
then (writeln"Adding rewrites:"; prths new_rws; ())
else ();
--- a/src/Provers/trancl.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Provers/trancl.ML Fri Mar 04 15:07:34 2005 +0100
@@ -327,7 +327,7 @@
(* Compute, for each adjacency list, the list with reversed edges,
and concatenate these lists. *)
- val flipped = Library.foldr (op @) ((map flip g),nil)
+ val flipped = foldr (op @) nil (map flip g)
in assemble g flipped end
@@ -351,9 +351,9 @@
let
val _ = visited := u :: !visited
val descendents =
- Library.foldr (fn ((v,l),ds) => if been_visited v then ds
+ foldr (fn ((v,l),ds) => if been_visited v then ds
else v :: dfs_visit g v @ ds)
- ( ((adjacent eq_comp g u)) ,nil)
+ nil (adjacent eq_comp g u)
in descendents end
in u :: dfs_visit g u end;
--- a/src/Provers/typedsimp.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Provers/typedsimp.ML Fri Mar 04 15:07:34 2005 +0100
@@ -70,7 +70,7 @@
handle THM _ => (simp_rls, rl :: other_rls);
(*Given the list rls, return the pair (simp_rls, other_rls).*)
-fun process_rules rls = Library.foldr add_rule (rls, ([],[]));
+fun process_rules rls = foldr add_rule ([],[]) rls;
(*Given list of rewrite rules, return list of both forms, reject others*)
fun process_rewrites rls =
--- a/src/Pure/General/lazy_seq.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/General/lazy_seq.ML Fri Mar 04 15:07:34 2005 +0100
@@ -397,8 +397,8 @@
make (fn () => copy (f x))
end
-fun EVERY fs = Library.foldr THEN (fs, succeed)
-fun FIRST fs = Library.foldr ORELSE (fs, fail)
+fun EVERY fs = foldr THEN succeed fs
+fun FIRST fs = foldr ORELSE fail fs
fun TRY f x =
make (fn () =>
--- a/src/Pure/General/name_space.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/General/name_space.ML Fri Mar 04 15:07:34 2005 +0100
@@ -102,7 +102,7 @@
error ("Attempt to declare hidden name " ^ quote name)
else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name);
-fun extend (NameSpace tab, names) = NameSpace (Library.foldr extend_aux (names, tab));
+fun extend (NameSpace tab, names) = NameSpace (foldr extend_aux tab names);
(* merge *) (*1st preferred over 2nd*)
@@ -126,7 +126,7 @@
Library.foldl (fn (tb, xname) => change del xname (name, tb))
(tab, if fully then accesses name else [base name])));
-fun hide fully (NameSpace tab, names) = NameSpace (Library.foldr (hide_aux fully) (names, tab));
+fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) tab names);
(* intern / extern names *)
--- a/src/Pure/General/seq.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/General/seq.ML Fri Mar 04 15:07:34 2005 +0100
@@ -97,7 +97,7 @@
| SOME (x, xq') => x :: list_of xq');
(*conversion from list to sequence*)
-fun of_list xs = Library.foldr cons (xs, empty);
+fun of_list xs = foldr cons empty xs;
(*map the function f over the sequence, making a new sequence*)
@@ -203,8 +203,8 @@
fun op APPEND (f, g) x =
append (f x, make (fn () => pull (g x)));
-fun EVERY fs = Library.foldr THEN (fs, succeed);
-fun FIRST fs = Library.foldr ORELSE (fs, fail);
+fun EVERY fs = foldr THEN succeed fs;
+fun FIRST fs = foldr ORELSE fail fs;
fun TRY f = ORELSE (f, succeed);
--- a/src/Pure/General/table.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/General/table.ML Fri Mar 04 15:07:34 2005 +0100
@@ -287,7 +287,7 @@
fun lookup_multi tab_key = getOpt (lookup tab_key,[]);
fun update_multi ((key, x), tab) = update ((key, x :: lookup_multi (tab, key)), tab);
-fun make_multi pairs = Library.foldr update_multi (pairs, empty);
+fun make_multi pairs = foldr update_multi empty pairs;
fun dest_multi tab = List.concat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));
fun merge_multi eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists eq xs xs')) tabs;
fun merge_multi' eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists' eq xs xs')) tabs;
--- a/src/Pure/IsaPlanner/isand.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/IsaPlanner/isand.ML Fri Mar 04 15:07:34 2005 +0100
@@ -108,7 +108,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 = Library.foldr allify_prem_var (Ts, p)
+ fun allify_prem Ts p = foldr allify_prem_var p Ts
val cTs = map (ctermify o Free) Ts
val cterm_asms = map (ctermify o allify_prem Ts) premts
@@ -167,7 +167,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 = Library.foldr allify_term (vs,t);
+ let val t_alls = foldr allify_term t vs;
val ct_alls = ctermify t_alls;
in
(ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
@@ -256,7 +256,7 @@
|> Drule.forall_intr_list cfvs
in Drule.compose_single (solth', i, gth) end;
-val export_solutions = Library.foldr (uncurry export_solution);
+fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
(* fix parameters of a subgoal "i", as free variables, and create an
--- a/src/Pure/IsaPlanner/rw_inst.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/IsaPlanner/rw_inst.ML Fri Mar 04 15:07:34 2005 +0100
@@ -124,7 +124,7 @@
fun mk_renamings tgt rule_inst =
let
val rule_conds = Thm.prems_of rule_inst
- val names = Library.foldr Term.add_term_names (tgt :: rule_conds, []);
+ val names = foldr Term.add_term_names [] (tgt :: rule_conds);
val (conds_tyvs,cond_vs) =
Library.foldl (fn ((tyvs, vs), t) =>
(Library.union
@@ -135,11 +135,11 @@
val termvars = map Term.dest_Var (Term.term_vars tgt);
val vars_to_fix = Library.union (termvars, cond_vs);
val (renamings, names2) =
- Library.foldr (fn (((n,i),ty), (vs, names')) =>
+ foldr (fn (((n,i),ty), (vs, names')) =>
let val n' = Term.variant names' n in
((((n,i),ty), Free (n', ty)) :: vs, n'::names')
end)
- (vars_to_fix, ([], names));
+ ([], names) vars_to_fix;
in renamings end;
(* make a new fresh typefree instantiation for the given tvar *)
@@ -152,12 +152,12 @@
already instantiated (in ignore_ixs) from the list of terms. *)
fun mk_fixtvar_tyinsts ignore_ixs ts =
let val (tvars, tfreenames) =
- Library.foldr (fn (t, (varixs, tfreenames)) =>
+ foldr (fn (t, (varixs, tfreenames)) =>
(Term.add_term_tvars (t,varixs),
Term.add_term_tfree_names (t,tfreenames)))
- (ts, ([],[]));
+ ([],[]) ts;
val unfixed_tvars = List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
- val (fixtyinsts, _) = Library.foldr new_tfree (unfixed_tvars, ([], tfreenames))
+ val (fixtyinsts, _) = foldr new_tfree ([], tfreenames) unfixed_tvars
in (fixtyinsts, tfreenames) end;
@@ -222,10 +222,10 @@
Term.subst_vars (typinsts,[]) outerterm;
(* type-instantiate the var instantiations *)
- val insts_tyinst = Library.foldr (fn ((ix,t),insts_tyinst) =>
+ val insts_tyinst = foldr (fn ((ix,t),insts_tyinst) =>
(ix, Term.subst_vars (typinsts,[]) t)
:: insts_tyinst)
- (unprepinsts,[]);
+ [] unprepinsts;
(* cross-instantiate *)
val insts_tyinst_inst = cross_inst insts_tyinst;
--- a/src/Pure/Isar/context_rules.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Isar/context_rules.ML Fri Mar 04 15:07:34 2005 +0100
@@ -203,7 +203,7 @@
fun gen_wrap which ctxt =
let val Rules {wrappers, ...} = LocalRules.get ctxt
- in fn tac => Library.foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
+ in fn tac => foldr (fn ((w, _), t) => w t) tac (which wrappers) end;
val Swrap = gen_wrap #1;
val wrap = gen_wrap #2;
--- a/src/Pure/Isar/locale.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Isar/locale.ML Fri Mar 04 15:07:34 2005 +0100
@@ -276,7 +276,7 @@
val cert = Thm.cterm_of sign;
val certT = Thm.ctyp_of sign;
val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
- val tfrees = Library.foldr Term.add_term_tfree_names (prop :: hyps, []);
+ val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env;
in
if null env' then th
@@ -395,7 +395,7 @@
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
fun inst_parms (i, ps) =
- Library.foldr Term.add_typ_tfrees (List.mapPartial snd ps, [])
+ foldr Term.add_typ_tfrees [] (List.mapPartial snd ps)
|> List.mapPartial (fn (a, S) =>
let val T = Envir.norm_type unifier' (TVar ((a, i), S))
in if T = TFree (a, S) then NONE else SOME ((a, S), T) end)
@@ -1049,7 +1049,7 @@
handle UnequalLengths => error "Number of parameters does not \
\match number of arguments of chained fact";
(* get their sorts *)
- val tfrees = Library.foldr Term.add_typ_tfrees (param_types, []);
+ val tfrees = foldr Term.add_typ_tfrees [] param_types
val Tenv' = map
(fn ((a, i), T) => ((a, valOf (assoc_string (tfrees, a))), T))
(Vartab.dest Tenv);
@@ -1076,7 +1076,7 @@
val cert = Thm.cterm_of sign;
val certT = Thm.ctyp_of sign;
val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
- val tfrees = Library.foldr Term.add_term_tfree_names (prop :: hyps, []);
+ val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
val Tenv' = List.filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
in
if null Tenv' then th
@@ -1278,7 +1278,7 @@
fun atomize_spec sign ts =
let
- val t = Library.foldr1 Logic.mk_conjunction ts;
+ val t = foldr1 Logic.mk_conjunction ts;
val body = ObjectLogic.atomize_term sign t;
val bodyT = Term.fastype_of body;
in
@@ -1308,7 +1308,7 @@
val env = Term.add_term_free_names (body, []);
val xs = List.filter (fn (x, _) => x mem_string env) parms;
val Ts = map #2 xs;
- val extraTs = (Term.term_tfrees body \\ Library.foldr Term.add_typ_tfrees (Ts, []))
+ val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
|> Library.sort_wrt #1 |> map TFree;
val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
--- a/src/Pure/Isar/method.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Isar/method.ML Fri Mar 04 15:07:34 2005 +0100
@@ -309,7 +309,7 @@
(* assumption *)
fun asm_tac ths =
- Library.foldr (op APPEND') (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths, K no_tac);
+ foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
fun assm_tac ctxt =
assume_tac APPEND'
--- a/src/Pure/Isar/net_rules.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Isar/net_rules.ML Fri Mar 04 15:07:34 2005 +0100
@@ -51,7 +51,7 @@
fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
let val rules = Library.gen_merge_lists' eq rules1 rules2
- in Library.foldr (uncurry add) (rules, init eq index) end;
+ in foldr (uncurry add) (init eq index) rules end;
fun delete rule (rs as Rules {eq, index, rules, next, net}) =
if not (Library.gen_mem eq (rule, rules)) then rs
--- a/src/Pure/Isar/proof.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Isar/proof.ML Fri Mar 04 15:07:34 2005 +0100
@@ -758,8 +758,8 @@
val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
val goal = Drule.mk_triv_goal cprop;
- val tvars = Library.foldr Term.add_term_tvars (props, []);
- val vars = Library.foldr Term.add_term_vars (props, []);
+ val tvars = foldr Term.add_term_tvars [] props;
+ val vars = foldr Term.add_term_vars [] props;
in
if null tvars then ()
else raise STATE ("Goal statement contains illegal schematic type variable(s): " ^
--- a/src/Pure/Isar/proof_context.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Mar 04 15:07:34 2005 +0100
@@ -697,7 +697,7 @@
val ins_occs = foldl_term_types (fn t => foldl_atyps
(fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab) | (tab, _) => tab));
-fun ins_skolem def_ty = Library.foldr
+fun ins_skolem def_ty = foldr
(fn ((x, x'), types) =>
(case def_ty x' of
SOME T => Vartab.update (((x, ~1), T), types)
@@ -716,7 +716,7 @@
declare_syn (ctxt, t)
|> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
|> map_defaults (fn (types, sorts, used, occ) =>
- (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, used, occ));
+ (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) types fixes, sorts, used, occ));
in
@@ -773,7 +773,7 @@
fun generalize inner outer ts =
let
- val tfrees = generalize_tfrees inner outer (Library.foldr Term.add_term_tfree_names (ts, []));
+ val tfrees = generalize_tfrees inner outer (foldr Term.add_term_tfree_names [] ts);
fun gen (x, S) = if x mem_string tfrees then TVar ((x, 0), S) else TFree (x, S);
in map (Term.map_term_types (Term.map_type_tfree gen)) ts end;
@@ -1267,8 +1267,8 @@
| replace [] ys = ys
| replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
in
- if null (Library.foldr Term.add_typ_tvars (map snd fixes, [])) andalso
- null (Library.foldr Term.add_term_vars (List.concat (map snd assumes), [])) then
+ if null (foldr Term.add_typ_tvars [] (map snd fixes)) andalso
+ null (foldr Term.add_term_vars [] (List.concat (map snd assumes))) then
{fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds}
else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
end;
--- a/src/Pure/Isar/rule_cases.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Isar/rule_cases.ML Fri Mar 04 15:07:34 2005 +0100
@@ -120,8 +120,8 @@
fun make is_open split (sg, prop) names =
let val nprems = Logic.count_prems (prop, 0) in
- Library.foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
- (Library.drop (length names - nprems, names), ([], length names)) |> #1
+ foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
+ ([], length names) (Library.drop (length names - nprems, names)) |> #1
end;
--- a/src/Pure/Proof/extraction.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Mar 04 15:07:34 2005 +0100
@@ -86,7 +86,7 @@
fun merge_rules
({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
- Library.foldr add_rule (rs2 \\ rs1, {next = next, rs = rs1, net = net});
+ foldr add_rule {next = next, rs = rs1, net = net} (rs2 \\ rs1);
fun condrew sign rules procs =
let
@@ -147,7 +147,7 @@
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in Abst (a, SOME T, prf_abstract_over t prf) end;
-val mkabs = Library.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
+val mkabs = foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
fun strip_abs 0 t = t
| strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
@@ -156,11 +156,11 @@
fun prf_subst_TVars tye =
map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
-fun relevant_vars types prop = Library.foldr (fn
+fun relevant_vars types prop = foldr (fn
(Var ((a, i), T), vs) => (case strip_type T of
(_, Type (s, _)) => if s mem types then a :: vs else vs
| _ => vs)
- | (_, vs) => vs) (vars_of prop, []);
+ | (_, vs) => vs) [] (vars_of prop);
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
@@ -254,7 +254,7 @@
defs, expand, prep} = ExtractionData.get thy;
in
ExtractionData.put
- {realizes_eqns = Library.foldr add_rule (map (prep_eq thy) eqns, realizes_eqns),
+ {realizes_eqns = foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
typeof_eqns = typeof_eqns, types = types, realizers = realizers,
defs = defs, expand = expand, prep = prep} thy
end
@@ -272,7 +272,7 @@
in
ExtractionData.put
{realizes_eqns = realizes_eqns, realizers = realizers,
- typeof_eqns = Library.foldr add_rule (eqns', typeof_eqns),
+ typeof_eqns = foldr add_rule typeof_eqns eqns',
types = types, defs = defs, expand = expand, prep = prep} thy
end
@@ -311,8 +311,8 @@
in
ExtractionData.put
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
- realizers = Library.foldr Symtab.update_multi
- (map (prep_rlz thy) (rev rs), realizers),
+ realizers = foldr Symtab.update_multi
+ realizers (map (prep_rlz thy) (rev rs)),
defs = defs, expand = expand, prep = prep} thy
end
@@ -344,7 +344,7 @@
(procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
(if T = nullT then t else list_comb (t, vars')) $ prop);
- val r = Library.foldr forall_intr (map (get_var_type r') vars, r');
+ val r = foldr forall_intr r' (map (get_var_type r') vars);
val prf = Reconstruct.reconstruct_proof sign r (rd s2);
in (name, (vs, (t, prf))) end
end;
@@ -448,7 +448,7 @@
end
else (vs', tye)
- in Library.foldr add_args (Library.take (n, vars) ~~ Library.take (n, ts), ([], [])) end;
+ in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
fun find vs = Option.map snd o find_first (curry eq_set vs o fst);
fun find' s = map snd o List.filter (equal s o fst)
@@ -543,10 +543,11 @@
val (defs'', corr_prf) =
corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
val corr_prop = Reconstruct.prop_of corr_prf;
- val corr_prf' = Library.foldr forall_intr_prf
- (map (get_var_type corr_prop) (vfs_of prop), proof_combt
+ val corr_prf' = foldr forall_intr_prf
+ (proof_combt
(PThm ((corr_name name vs', []), corr_prf, corr_prop,
SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
+ (map (get_var_type corr_prop) (vfs_of prop))
in
((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
prf_subst_TVars tye' corr_prf')
@@ -630,11 +631,11 @@
val args = filter_out (fn v => tname_of (body_type
(fastype_of v)) mem rtypes) (vfs_of prop);
val args' = List.filter (fn v => Logic.occs (v, nt)) args;
- val t' = mkabs (args', nt);
+ val t' = mkabs nt args';
val T = fastype_of t';
val cname = extr_name s vs';
val c = Const (cname, T);
- val u = mkabs (args, list_comb (c, args'));
+ val u = mkabs (list_comb (c, args')) args;
val eqn = Logic.mk_equals (c, t');
val rlz =
Const ("realizes", fastype_of nt --> propT --> propT);
@@ -651,10 +652,11 @@
PAxm (cname ^ "_def", eqn,
SOME (map TVar (term_tvars eqn))))) %% corr_prf;
val corr_prop = Reconstruct.prop_of corr_prf';
- val corr_prf'' = Library.foldr forall_intr_prf
- (map (get_var_type corr_prop) (vfs_of prop), proof_combt
+ val corr_prf'' = foldr forall_intr_prf
+ (proof_combt
(PThm ((corr_name s vs', []), corr_prf', corr_prop,
- SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop));
+ SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
+ (map (get_var_type corr_prop) (vfs_of prop));
in
((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
subst_TVars tye' u)
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Mar 04 15:07:34 2005 +0100
@@ -228,7 +228,7 @@
val tvars = term_tvars prop;
val (_, rhs) = Logic.dest_equals prop;
val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
- (Library.foldr (fn p => Abs ("", dummyT, abstract_over p)) (vs, rhs)),
+ (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
map valOf ts);
in
change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
--- a/src/Pure/Proof/proof_syntax.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 04 15:07:34 2005 +0100
@@ -97,10 +97,10 @@
val tab = Symtab.foldl (fn (tab, (key, ps)) =>
let val prop = getOpt (assoc (thms', key), Bound 0)
- in fst (Library.foldr (fn ((prop', prf), x as (tab, i)) =>
+ in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
if prop <> prop' then
(Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
- else x) (ps, (tab, 1)))
+ else x) (tab, 1) ps)
end) (Symtab.empty, thms);
fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
--- a/src/Pure/Proof/proofchecker.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Proof/proofchecker.ML Fri Mar 04 15:07:34 2005 +0100
@@ -19,8 +19,8 @@
(***** construct a theorem out of a proof term *****)
fun lookup_thm thy =
- let val tab = Library.foldr Symtab.update
- (List.concat (map thms_of (thy :: Theory.ancestors_of thy)), Symtab.empty)
+ let val tab = foldr Symtab.update Symtab.empty
+ (List.concat (map thms_of (thy :: Theory.ancestors_of thy)))
in
(fn s => case Symtab.lookup (tab, s) of
NONE => error ("Unknown theorem " ^ quote s)
--- a/src/Pure/Proof/reconstruct.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Proof/reconstruct.ML Fri Mar 04 15:07:34 2005 +0100
@@ -30,15 +30,15 @@
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in all T $ Abs (a, T, abstract_over (t, prop)) end;
-fun forall_intr_vfs prop = Library.foldr forall_intr
- (vars_of prop @ sort (make_ord atless) (term_frees prop), prop);
+fun forall_intr_vfs prop = foldr forall_intr prop
+ (vars_of prop @ sort (make_ord atless) (term_frees prop));
fun forall_intr_prf (t, prf) =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in Abst (a, SOME T, prf_abstract_over t prf) end;
-fun forall_intr_vfs_prf prop prf = Library.foldr forall_intr_prf
- (vars_of prop @ sort (make_ord atless) (term_frees prop), prf);
+fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf prf
+ (vars_of prop @ sort (make_ord atless) (term_frees prop));
fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
(Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
--- a/src/Pure/Syntax/printer.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Syntax/printer.ML Fri Mar 04 15:07:34 2005 +0100
@@ -246,7 +246,7 @@
let
val fmts = List.mapPartial xprod_to_fmt xprods;
val tab = get_tab prtabs mode;
- val new_tab = Library.foldr Symtab.update_multi (rev fmts, tab);
+ val new_tab = foldr Symtab.update_multi tab (rev fmts);
in overwrite (prtabs, (mode, new_tab)) end;
fun merge_prtabs prtabs1 prtabs2 =
--- a/src/Pure/Syntax/syntax.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/Syntax/syntax.ML Fri Mar 04 15:07:34 2005 +0100
@@ -101,7 +101,7 @@
(* print (ast) translations *)
fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
-fun extend_tr'tab tab trfuns = Library.foldr Symtab.update_multi (map mk_trfun trfuns, tab);
+fun extend_tr'tab tab trfuns = foldr Symtab.update_multi tab (map mk_trfun trfuns);
fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' eq_trfuns (tab1, tab2);
@@ -154,7 +154,7 @@
(* empty, extend, merge ruletabs *)
fun extend_ruletab tab rules =
- Library.foldr Symtab.update_multi (map (fn r => (Ast.head_of_rule r, r)) rules, tab);
+ foldr Symtab.update_multi tab (map (fn r => (Ast.head_of_rule r, r)) rules);
fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
--- a/src/Pure/codegen.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/codegen.ML Fri Mar 04 15:07:34 2005 +0100
@@ -225,8 +225,8 @@
fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
val code_attr =
- Attrib.syntax (Scan.depend (fn thy => Library.foldr op || (map mk_parser
- (#attrs (CodegenData.get thy)), Scan.fail) >> pair thy));
+ Attrib.syntax (Scan.depend (fn thy => foldr op || Scan.fail (map mk_parser
+ (#attrs (CodegenData.get thy))) >> pair thy));
(**** preprocessors ****)
@@ -344,8 +344,8 @@
fun rename_terms ts =
let
- val names = Library.foldr add_term_names
- (ts, map (fst o fst) (Drule.vars_of_terms ts));
+ val names = foldr add_term_names
+ (map (fst o fst) (Drule.vars_of_terms ts)) ts;
val reserved = names inter ThmDatabase.ml_reserved;
val (illegal, alt_names) = split_list (List.mapPartial (fn s =>
let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
@@ -443,8 +443,8 @@
val (Ts, _) = strip_type (fastype_of t);
val j = i - length ts
in
- Library.foldr (fn (T, t) => Abs ("x", T, t))
- (Library.take (j, Ts), list_comb (t, ts @ map Bound (j-1 downto 0)))
+ foldr (fn (T, t) => Abs ("x", T, t))
+ (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
end;
fun mk_app _ p [] = p
--- a/src/Pure/display.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/display.ML Fri Mar 04 15:07:34 2005 +0100
@@ -282,7 +282,7 @@
| add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
| add_vars (_, env) = env;
-fun add_varsT (Type (_, Ts), env) = Library.foldr add_varsT (Ts, env)
+fun add_varsT (Type (_, Ts), env) = foldr add_varsT env Ts
| add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
| add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
--- a/src/Pure/drule.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/drule.ML Fri Mar 04 15:07:34 2005 +0100
@@ -343,10 +343,10 @@
in Library.foldl elim (thm, Term.variantlist (map #1 vs, []) ~~ map #2 vs) end;
(*Specialization over a list of cterms*)
-fun forall_elim_list cts th = Library.foldr (uncurry forall_elim) (rev cts, th);
+fun forall_elim_list cts th = foldr (uncurry forall_elim) th (rev cts);
(* maps A1,...,An |- B to [| A1;...;An |] ==> B *)
-fun implies_intr_list cAs th = Library.foldr (uncurry implies_intr) (cAs,th);
+fun implies_intr_list cAs th = foldr (uncurry implies_intr) th cAs;
(* maps [| A1;...;An |] ==> B and [A1,...,An] to B *)
fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
@@ -364,12 +364,12 @@
fun zero_var_indexes th =
let val {prop,sign,tpairs,...} = rep_thm th;
val (tpair_l, tpair_r) = Library.split_list tpairs;
- val vars = Library.foldr add_term_vars
- (tpair_r, Library.foldr add_term_vars (tpair_l, (term_vars prop)));
+ val vars = foldr add_term_vars
+ (foldr add_term_vars (term_vars prop) tpair_l) tpair_r;
val bs = Library.foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
val inrs =
- Library.foldr add_term_tvars
- (tpair_r, Library.foldr add_term_tvars (tpair_l, (term_tvars prop)));
+ foldr add_term_tvars
+ (foldr add_term_tvars (term_tvars prop) tpair_l) tpair_r;
val nms' = rev(Library.foldl add_new_id ([], map (#1 o #1) inrs));
val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
(inrs, nms')
@@ -423,13 +423,13 @@
let val fth = freezeT th
val {prop, tpairs, sign, ...} = rep_thm fth
in
- case Library.foldr add_term_vars (prop :: Thm.terms_of_tpairs tpairs, []) of
+ case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
[] => (fth, fn i => fn x => x) (*No vars: nothing to do!*)
| vars =>
let fun newName (Var(ix,_), pairs) =
let val v = gensym (string_of_indexname ix)
in ((ix,v)::pairs) end;
- val alist = Library.foldr newName (vars,[])
+ val alist = foldr newName [] vars
fun mk_inst (Var(v,T)) =
(cterm_of sign (Var(v,T)),
cterm_of sign (Free(valOf (assoc(alist,v)), T)))
@@ -446,14 +446,14 @@
let val fth = freezeT th
val {prop, tpairs, sign, ...} = rep_thm fth
in
- case Library.foldr add_term_vars (prop :: Thm.terms_of_tpairs tpairs, []) of
+ case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
[] => (fth, fn x => x)
| vars =>
let fun newName (Var(ix,_), (pairs,used)) =
let val v = variant used (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
- val (alist, _) = Library.foldr newName (vars, ([], Library.foldr add_term_names
- (prop :: Thm.terms_of_tpairs tpairs, [])))
+ val (alist, _) = foldr newName ([], Library.foldr add_term_names
+ (prop :: Thm.terms_of_tpairs tpairs, [])) vars
fun mk_inst (Var(v,T)) =
(cterm_of sign (Var(v,T)),
cterm_of sign (Free(valOf (assoc(alist,v)), T)))
@@ -641,9 +641,9 @@
fun abs_def thm =
let
val (_, cvs) = strip_comb (fst (dest_equals (cprop_of thm)));
- val thm' = Library.foldr (fn (ct, thm) => Thm.abstract_rule
+ val thm' = foldr (fn (ct, thm) => Thm.abstract_rule
(case term_of ct of Var ((a, _), _) => a | Free (a, _) => a | _ => "x")
- ct thm) (cvs, thm)
+ ct thm) thm cvs
in transitive
(symmetric (eta_conversion (fst (dest_equals (cprop_of thm'))))) thm'
end;
@@ -835,7 +835,7 @@
in (sign', tye', maxi') end;
in
fun cterm_instantiate ctpairs0 th =
- let val (sign,tye,_) = Library.foldr add_types (ctpairs0, (Thm.sign_of_thm th, Vartab.empty, 0))
+ let val (sign,tye,_) = foldr add_types (Thm.sign_of_thm th, Vartab.empty, 0) ctpairs0
fun instT(ct,cu) =
let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
in (inst ct, inst cu) end
@@ -862,7 +862,7 @@
handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
(*Calling equal_abs_elim with multiple terms*)
-fun equal_abs_elim_list cts th = Library.foldr (uncurry equal_abs_elim) (rev cts, th);
+fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) th (rev cts);
(*** Goal (PROP A) <==> PROP A ***)
@@ -991,7 +991,7 @@
fun tfrees_of thm =
let val {hyps, prop, ...} = Thm.rep_thm thm
- in Library.foldr Term.add_term_tfree_names (prop :: hyps, []) end;
+ in foldr Term.add_term_tfree_names [] (prop :: hyps) end;
fun tvars_intr_list tfrees thm =
Thm.varifyT' (tfrees_of thm \\ tfrees) thm;
--- a/src/Pure/goals.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/goals.ML Fri Mar 04 15:07:34 2005 +0100
@@ -307,8 +307,8 @@
let val cur_sc = get_scope_sg sg;
val rule_lists = map (#rules o snd) cur_sc;
val def_lists = map (#defs o snd) cur_sc;
- val rules = map snd (Library.foldr (op union) (rule_lists, []));
- val defs = map snd (Library.foldr (op union) (def_lists, []));
+ val rules = map snd (foldr (op union) [] rule_lists);
+ val defs = map snd (foldr (op union) [] def_lists);
val defnrules = rules @ defs;
in
hyps subset defnrules
--- a/src/Pure/meta_simplifier.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/meta_simplifier.ML Fri Mar 04 15:07:34 2005 +0100
@@ -1059,9 +1059,9 @@
find_index_eq p tprems) (#hyps (rep_thm eqn)));
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
- (rrs' :: rrss') (asm' :: asms') (SOME (Library.foldr (disch true)
- (Library.take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies
- (Library.drop (i, prems), concl))))) :: eqns) ss (length prems') ~1
+ (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)
+ (Drule.imp_cong' eqn (reflexive (Drule.list_implies
+ (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns) ss (length prems') ~1
end
(*legacy code - only for backwards compatibility*)
--- a/src/Pure/net.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/net.ML Fri Mar 04 15:07:34 2005 +0100
@@ -165,9 +165,9 @@
(*Skipping a term in a net. Recursively skip 2 levels if a combination*)
fun net_skip (Leaf _, nets) = nets
| net_skip (Net{comb,var,alist}, nets) =
- Library.foldr net_skip
- (net_skip (comb,[]),
- Library.foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
+ foldr net_skip
+ (foldr (fn ((_,net), nets) => net::nets) (var::nets) alist)
+ (net_skip (comb,[]))
(** Matching and Unification**)
@@ -185,7 +185,7 @@
let fun rands _ (Leaf _, nets) = nets
| rands t (Net{comb,alist,...}, nets) =
case t of
- f$t => Library.foldr (matching unif t) (rands f (comb,[]), nets)
+ f$t => foldr (matching unif t) nets (rands f (comb,[]))
| Const(c,_) => look1 (alist, c) nets
| Free(c,_) => look1 (alist, c) nets
| Bound i => look1 (alist, string_of_bound i) nets
--- a/src/Pure/pattern.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/pattern.ML Fri Mar 04 15:07:34 2005 +0100
@@ -476,7 +476,7 @@
val skel0 = Bound 0;
val rhs_names =
- Library.foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) (rules, []);
+ foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) [] rules;
fun variant_absfree (x, T, t) =
let
--- a/src/Pure/proofterm.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/proofterm.ML Fri Mar 04 15:07:34 2005 +0100
@@ -217,7 +217,7 @@
(PThm (_, prf', _, _), _) => prf'
| _ => prf);
-val mk_Abst = Library.foldr (fn ((s, T:typ), prf) => Abst (s, NONE, prf));
+val mk_Abst = foldr (fn ((s, T:typ), prf) => Abst (s, NONE, prf));
fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
fun apsome' f NONE = raise SAME
@@ -254,8 +254,8 @@
| fold_proof_terms f g (a, prf % NONE) = fold_proof_terms f g (a, prf)
| fold_proof_terms f g (a, prf1 %% prf2) = fold_proof_terms f g
(fold_proof_terms f g (a, prf1), prf2)
- | fold_proof_terms _ g (a, PThm (_, _, _, SOME Ts)) = Library.foldr g (Ts, a)
- | fold_proof_terms _ g (a, PAxm (_, prop, SOME Ts)) = Library.foldr g (Ts, a)
+ | fold_proof_terms _ g (a, PThm (_, _, _, SOME Ts)) = foldr g a Ts
+ | fold_proof_terms _ g (a, PAxm (_, prop, SOME Ts)) = foldr g a Ts
| fold_proof_terms _ _ (a, _) = a;
val add_prf_names = fold_proof_terms add_term_names ((uncurry K) o swap);
@@ -557,7 +557,7 @@
let
val used = it_term_types add_typ_tfree_names (t, [])
and tvars = map #1 (it_term_types add_typ_tvars (t, []));
- val (alist, _) = Library.foldr new_name (tvars, ([], used));
+ val (alist, _) = foldr new_name ([], used) tvars;
in
(case alist of
[] => prf (*nothing to do!*)
@@ -579,9 +579,9 @@
val j = length Bs;
in
mk_AbsP (j+1, proof_combP (prf, map PBound
- (j downto 1) @ [mk_Abst (params, mk_AbsP (i,
+ (j downto 1) @ [mk_Abst (mk_AbsP (i,
proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
- map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
+ map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m)))))) params]))
end;
@@ -637,7 +637,7 @@
| lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
| lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
- map (fn k => (#3 (Library.foldr mk_app (bs, (i-1, j-1, PBound k)))))
+ map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
(i + k - 1 downto i));
in
mk_AbsP (k, lift [] [] 0 0 Bi)
@@ -1127,7 +1127,7 @@
map SOME (sort (make_ord atless) (term_frees prop));
val opt_prf = if ! proofs = 2 then
#4 (shrink [] 0 (rewrite_prf fst (ProofData.get_sg sign)
- (Library.foldr (uncurry implies_intr_proof) (hyps, prf))))
+ (foldr (uncurry implies_intr_proof) prf hyps)))
else MinProof (mk_min_proof ([], prf));
val head = (case strip_combt (fst (strip_combP prf)) of
(PThm ((old_name, _), prf', prop', NONE), args') =>
--- a/src/Pure/search.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/search.ML Fri Mar 04 15:07:34 2005 +0100
@@ -215,8 +215,8 @@
fun pairsize th = (sizef th, th);
fun bfs (news,nprf_heap) =
(case List.partition satp news of
- ([],nonsats) => next(Library.foldr ThmHeap.insert
- (map pairsize nonsats, nprf_heap))
+ ([],nonsats) => next(foldr ThmHeap.insert
+ nprf_heap (map pairsize nonsats))
| (sats,_) => some_of_list sats)
and next nprf_heap =
if ThmHeap.is_empty nprf_heap then NONE
@@ -277,7 +277,7 @@
let fun cost thm = (level, costf level thm, thm)
in (case List.partition satp news of
([],nonsats)
- => next (Library.foldr insert_with_level (map cost nonsats, nprfs))
+ => next (foldr insert_with_level nprfs (map cost nonsats))
| (sats,_) => some_of_list sats)
end and
next [] = NONE
--- a/src/Pure/sign.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/sign.ML Fri Mar 04 15:07:34 2005 +0100
@@ -832,7 +832,7 @@
let
val tsig = tsig_of sg;
- val termss = Library.foldr multiply (map fst args, [[]]);
+ val termss = foldr multiply [[]] (map fst args);
val typs =
map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
--- a/src/Pure/tactic.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/tactic.ML Fri Mar 04 15:07:34 2005 +0100
@@ -426,7 +426,7 @@
(*build a pair of nets for biresolution*)
fun build_netpair netpair brls =
- Library.foldr insert_tagged_brl (taglist 1 brls, netpair);
+ foldr insert_tagged_brl netpair (taglist 1 brls);
(*delete one kbrl from the pair of nets*)
local
@@ -473,7 +473,7 @@
(*build a net of rules for resolution*)
fun build_net rls =
- Library.foldr insert_krl (taglist 1 rls, Net.empty);
+ foldr insert_krl Net.empty (taglist 1 rls);
(*resolution using a net rather than rules; pred supports filt_resolve_tac*)
fun filt_resolution_from_net_tac match pred net =
@@ -644,7 +644,7 @@
val statement = Logic.list_implies (asms, prop);
val frees = map Term.dest_Free (Term.term_frees statement);
val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
- val fixed_tfrees = Library.foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
+ val fixed_tfrees = foldr Term.add_typ_tfree_names [] (map #2 fixed_frees);
val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
fun err msg = raise ERROR_MESSAGE
--- a/src/Pure/tctical.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/tctical.ML Fri Mar 04 15:07:34 2005 +0100
@@ -179,10 +179,10 @@
fun EVERY1 tacs = EVERY' tacs 1;
(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *)
-fun FIRST tacs = Library.foldr (op ORELSE) (tacs, no_tac);
+fun FIRST tacs = foldr (op ORELSE) no_tac tacs;
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *)
-fun FIRST' tacs = Library.foldr (op ORELSE') (tacs, K no_tac);
+fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs;
(*Apply first tactic to 1*)
fun FIRST1 tacs = FIRST' tacs 1;
@@ -439,7 +439,7 @@
let val {sign,maxidx,...} = rep_thm state
val cterm = cterm_of sign
(*find all vars in the hyps -- should find tvars also!*)
- val hyps_vars = Library.foldr add_term_vars (Logic.strip_assums_hyp prem, [])
+ val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem)
val insts = map mk_inst hyps_vars
(*replace the hyps_vars by Frees*)
val prem' = subst_atomic insts prem
@@ -472,7 +472,7 @@
fun relift st =
let val prop = #prop(rep_thm st)
val subgoal_vars = (*Vars introduced in the subgoals*)
- Library.foldr add_term_vars (Logic.strip_imp_prems prop, [])
+ foldr add_term_vars [] (Logic.strip_imp_prems prop)
and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
--- a/src/Pure/term.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/term.ML Fri Mar 04 15:07:34 2005 +0100
@@ -773,11 +773,11 @@
(** Consts etc. **)
-fun add_typ_classes (Type (_, Ts), cs) = Library.foldr add_typ_classes (Ts, cs)
+fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
| add_typ_classes (TFree (_, S), cs) = S union cs
| add_typ_classes (TVar (_, S), cs) = S union cs;
-fun add_typ_tycons (Type (c, Ts), cs) = Library.foldr add_typ_tycons (Ts, c ins cs)
+fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins cs) Ts
| add_typ_tycons (_, cs) = cs;
val add_term_classes = it_term_types add_typ_classes;
@@ -840,20 +840,20 @@
| add_term_names (_, bs) = bs;
(*Accumulates the TVars in a type, suppressing duplicates. *)
-fun add_typ_tvars(Type(_,Ts),vs) = Library.foldr add_typ_tvars (Ts,vs)
+fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
| add_typ_tvars(TFree(_),vs) = vs
| add_typ_tvars(TVar(v),vs) = v ins vs;
(*Accumulates the TFrees in a type, suppressing duplicates. *)
-fun add_typ_tfree_names(Type(_,Ts),fs) = Library.foldr add_typ_tfree_names (Ts,fs)
+fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
| add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
| add_typ_tfree_names(TVar(_),fs) = fs;
-fun add_typ_tfrees(Type(_,Ts),fs) = Library.foldr add_typ_tfrees (Ts,fs)
+fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
| add_typ_tfrees(TFree(f),fs) = f ins fs
| add_typ_tfrees(TVar(_),fs) = fs;
-fun add_typ_varnames(Type(_,Ts),nms) = Library.foldr add_typ_varnames (Ts,nms)
+fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
| add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
| add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
--- a/src/Pure/thm.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/thm.ML Fri Mar 04 15:07:34 2005 +0100
@@ -977,8 +977,8 @@
No longer normalizes the new theorem! *)
fun instantiate ([], []) th = th
| instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) =
- let val (newsign_ref,tpairs) = Library.foldr add_ctpair (ctpairs, (sign_ref,[]));
- val (newsign_ref,vTs) = Library.foldr add_ctyp (vcTs, (newsign_ref,[]));
+ let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs;
+ val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs;
fun subst t =
subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t);
val newprop = subst prop;
@@ -1041,7 +1041,7 @@
(* Replace all TFrees not fixed or in the hyps by new TVars *)
fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
let
- val tfrees = Library.foldr add_term_tfree_names (hyps, fixed);
+ val tfrees = foldr add_term_tfree_names fixed hyps;
val prop1 = attach_tpairs tpairs prop;
val (prop2, al) = Type.varify (prop1, tfrees);
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
@@ -1282,8 +1282,8 @@
Preserves unknowns in tpairs and on lhs of dpairs. *)
fun rename_bvs([],_,_,_) = I
| rename_bvs(al,dpairs,tpairs,B) =
- let val vars = Library.foldr add_term_vars
- (map fst dpairs @ map fst tpairs @ map snd tpairs, [])
+ let val vars = foldr add_term_vars []
+ (map fst dpairs @ map fst tpairs @ map snd tpairs)
(*unknowns appearing elsewhere be preserved!*)
val vids = map (#1 o #1 o dest_Var) vars;
fun rename(t as Var((x,i),T)) =
@@ -1300,7 +1300,7 @@
(*Function to rename bounds/unknowns in the argument, lifted over B*)
fun rename_bvars(dpairs, tpairs, B) =
- rename_bvs(Library.foldr Term.match_bvars (dpairs,[]), dpairs, tpairs, B);
+ rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
(*** RESOLUTION ***)
--- a/src/Pure/type.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/type.ML Fri Mar 04 15:07:34 2005 +0100
@@ -252,14 +252,14 @@
let
val used = add_typ_tfree_names (T, [])
and tvars = map #1 (add_typ_tvars (T, []));
- val (alist, _) = Library.foldr new_name (tvars, ([], used));
+ val (alist, _) = foldr new_name ([], used) tvars;
in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
fun freeze_thaw t =
let
val used = it_term_types add_typ_tfree_names (t, [])
and tvars = map #1 (it_term_types add_typ_tvars (t, []));
- val (alist, _) = Library.foldr new_name (tvars, ([], used));
+ val (alist, _) = foldr new_name ([], used) tvars;
in
(case alist of
[] => (t, fn x => x) (*nothing to do!*)
@@ -378,7 +378,7 @@
else meet ((T, S), Vartab.update_new ((v, T), tye))
| (Type (a, Ts), Type (b, Us)) =>
if a <> b then raise TUNIFY
- else Library.foldr unif (Ts ~~ Us, tye)
+ else foldr unif tye (Ts ~~ Us)
| (T, U) => if T = U then tye else raise TUNIFY);
in (unif (TU, tyenv), ! tyvar_count) end;
--- a/src/Pure/unify.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/unify.ML Fri Mar 04 15:07:34 2005 +0100
@@ -291,7 +291,7 @@
Clever would be to re-do just the affected dpairs*)
fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
let val all as (env',flexflex,flexrigid) =
- Library.foldr SIMPL0 (dpairs, (env,[],[]));
+ foldr SIMPL0 (env,[],[]) dpairs;
val dps = flexrigid@flexflex
in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
then SIMPL(env',dps) else all
@@ -488,7 +488,7 @@
val (Ts,U) = strip_type env T
and js = length ts - 1 downto 0
val args = sort (make_ord arg_less)
- (Library.foldr (change_arg banned) (flexargs (js,ts,Ts), []))
+ (foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
val ts' = map (#t) args
in
if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
@@ -521,7 +521,7 @@
then (bnos, (a,T)::newbinder) (*needed by both: keep*)
else (j::bnos, newbinder); (*remove*)
val indices = 0 upto (length rbinder - 1);
- val (banned,rbin') = Library.foldr add_index (rbinder~~indices, ([],[]));
+ val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices);
val (env', t') = clean_term banned (env, t);
val (env'',u') = clean_term banned (env',u)
in (ff_assign(env'', rbin', t', u'), tpairs)
@@ -575,7 +575,7 @@
then print_dpairs "Enter SIMPL" (env,dpairs) else ();
SIMPL (env,dpairs))
in case flexrigid of
- [] => SOME (Library.foldr add_ffpair (flexflex, (env',[])), reseq)
+ [] => SOME (foldr add_ffpair (env',[]) flexflex, reseq)
| dp::frigid' =>
if tdepth > !search_bound then
(warning "Unification bound exceeded"; Seq.pull reseq)
@@ -626,7 +626,7 @@
(*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*)
fun smash_flexflex (env,tpairs) : Envir.env =
- Library.foldr smash_flexflex1 (tpairs, env);
+ foldr smash_flexflex1 env tpairs;
(*Returns unifiers with no remaining disagreement pairs*)
fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
--- a/src/ZF/Tools/datatype_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/ZF/Tools/datatype_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -126,11 +126,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) = Library.foldr add_case (con_ty_list, (opno, []))
+ let val (opno', case_list) = foldr add_case (opno, []) con_ty_list
in (opno', case_list :: case_lists) end;
(*Treatment of all parts*)
- val (_, case_lists) = Library.foldr add_case_list (con_ty_lists, (1,[]));
+ val (_, case_lists) = 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) ---> (iT-->iT);
@@ -170,9 +170,9 @@
val rec_args = map (make_rec_call (rev case_args,0))
(List.drop(recursor_args, ncase_args))
in
- Library.foldr add_abs
- (case_args, list_comb (recursor_var,
- bound_args @ rec_args))
+ foldr add_abs
+ (list_comb (recursor_var,
+ bound_args @ rec_args)) case_args
end
(*Find each recursive argument and add a recursive call for it*)
@@ -202,7 +202,7 @@
val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
(*Treatment of all parts*)
- val (_, recursor_lists) = Library.foldr add_case_list (rec_ty_lists, (1,[]));
+ val (_, recursor_lists) = 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)
@@ -384,7 +384,7 @@
(("free_iffs", free_iffs), []),
(("free_elims", free_SEs), [])])
|> DatatypesData.map (fn tab => Symtab.update ((big_rec_name, dt_info), tab))
- |> ConstructorsData.map (fn tab => Library.foldr Symtab.update (con_pairs, tab))
+ |> ConstructorsData.map (fn tab => foldr Symtab.update tab con_pairs)
|> Theory.parent_path,
ind_result,
{con_defs = con_defs,
--- a/src/ZF/Tools/induct_tacs.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Fri Mar 04 15:07:34 2005 +0100
@@ -178,7 +178,7 @@
(Symtab.update
((big_rec_name, dt_info), DatatypesData.get thy))
|> ConstructorsData.put
- (Library.foldr Symtab.update (con_pairs, ConstructorsData.get thy))
+ (foldr Symtab.update (ConstructorsData.get thy) con_pairs)
|> Theory.parent_path
end;
--- a/src/ZF/Tools/inductive_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/ZF/Tools/inductive_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -102,7 +102,7 @@
Sign.string_of_term sign t);
(*** Construct the fixedpoint definition ***)
- val mk_variant = variant (Library.foldr add_term_names (intr_tms, []));
+ val mk_variant = variant (foldr add_term_names [] intr_tms);
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
@@ -116,8 +116,8 @@
val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
val exfrees = term_frees intr \\ rec_params
val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
- in Library.foldr FOLogic.mk_exists
- (exfrees, fold_bal FOLogic.mk_conj (zeq::prems))
+ in foldr FOLogic.mk_exists
+ (fold_bal FOLogic.mk_conj (zeq::prems)) exfrees
end;
(*The Part(A,h) terms -- compose injections to make h*)
@@ -311,8 +311,8 @@
(*Make a premise of the induction rule.*)
fun induct_prem ind_alist intr =
let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
- val iprems = Library.foldr (add_induct_prem ind_alist)
- (Logic.strip_imp_prems intr,[])
+ val iprems = foldr (add_induct_prem ind_alist) []
+ (Logic.strip_imp_prems intr)
val (t,X) = Ind_Syntax.rule_concl intr
val (SOME pred) = gen_assoc (op aconv) (ind_alist, X)
val concl = FOLogic.mk_Trueprop (pred $ t)
@@ -390,11 +390,10 @@
val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
elem_factors ---> FOLogic.oT)
val qconcl =
- Library.foldr FOLogic.mk_all
- (elem_frees,
- FOLogic.imp $
+ foldr FOLogic.mk_all
+ (FOLogic.imp $
(Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
- $ (list_comb (pfree, elem_frees)))
+ $ (list_comb (pfree, elem_frees))) elem_frees
in (CP.ap_split elem_type FOLogic.oT pfree,
qconcl)
end;
--- a/src/ZF/Tools/primrec_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/ZF/Tools/primrec_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -128,7 +128,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 = Library.foldr absterm (allowed_terms, rhs)
+ val abs = foldr absterm rhs allowed_terms
in
if !Ind_Syntax.trace then
writeln ("recursor_rhs = " ^
@@ -153,7 +153,7 @@
val def_tm = Logic.mk_equals
(subst_bound (rec_arg, fabs),
list_comb (recursor,
- Library.foldr add_case (cnames ~~ recursor_pairs, []))
+ foldr add_case [] (cnames ~~ recursor_pairs))
$ rec_arg)
in
@@ -172,7 +172,7 @@
let
val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
val SOME (fname, ftype, ls, rs, con_info, eqns) =
- Library.foldr (process_eqn thy) (eqn_terms, NONE);
+ foldr (process_eqn thy) NONE eqn_terms;
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
val (thy1, [def_thm]) = thy