# HG changeset patch # User skalberg # Date 1109945254 -3600 # Node ID b1d1b5bfc46448fcfe597f1030a7e287202e0979 # Parent cf53c2dcf440790a0461058fb7ab6f6d090e1eaa Removed practically all references to Library.foldr. diff -r cf53c2dcf440 -r b1d1b5bfc464 TFL/post.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 TFL/rules.ML --- 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! *) diff -r cf53c2dcf440 -r b1d1b5bfc464 TFL/tfl.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 etc/settings --- 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") diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/convert --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/expandshort --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/fixclasimp --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/fixdatatype --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/fixdots --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/fixgoal --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/fixgreek --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/fixseq --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/fixsome --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/install --- 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 /*) diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/logo --- 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//$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps" diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/mkdir --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 lib/Tools/unsymbolize --- 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" diff -r cf53c2dcf440 -r b1d1b5bfc464 src/FOLP/simp.ML --- 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 (); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Import/proof_kernel.ML --- 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' diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Import/replay.ML --- 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'' diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Import/shuffler.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Integ/cooper_dec.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Integ/presburger.ML --- 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 --*) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Library/EfficientNat.thy --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Matrix/eq_codegen.ML --- 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); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Modelcheck/mucke_oracle.ML --- 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)); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/Presburger/cooper_dec.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/Presburger/presburger.ML --- 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 --*) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/datatype_abs_proofs.ML --- 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'); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/datatype_aux.ML --- 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) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/datatype_codegen.ML --- 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) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/datatype_package.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/datatype_prop.ML --- 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) => diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/datatype_realizer.ML --- 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]))))); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/datatype_rep_proofs.ML --- 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 *) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/inductive_codegen.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/inductive_package.ML --- 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 *) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/inductive_realizer.ML --- 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) = diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/meson.ML --- 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.*) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/primrec_package.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/recdef_package.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/recfun_codegen.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/record_package.ML --- 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 *) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/refute.ML --- 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 ("", T, t)) - (Library.take (i, Ts), list_comb (t, map Bound (i-1 downto 0))) + foldr (fn (T, t) => Abs ("", 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/specification_package.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/Tools/split_rule.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/ex/svc_funcs.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOL/hologic.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOLCF/domain/axioms.ML --- 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) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOLCF/domain/library.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/HOLCF/domain/syntax.ML --- 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, diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Provers/blast.ML --- 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*) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Provers/classical.ML --- 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); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Provers/induct_method.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Provers/order.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Provers/simp.ML --- 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 (); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Provers/trancl.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Provers/typedsimp.ML --- 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 = diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/General/lazy_seq.ML --- 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 () => diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/General/name_space.ML --- 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 *) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/General/seq.ML --- 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); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/General/table.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/IsaPlanner/isand.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/IsaPlanner/rw_inst.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Isar/context_rules.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Isar/locale.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Isar/method.ML --- 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' diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Isar/net_rules.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Isar/proof.ML --- 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): " ^ diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Isar/proof_context.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Isar/rule_cases.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Proof/extraction.ML --- 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) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Proof/proof_rewrite_rules.ML --- 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' diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Proof/proof_syntax.ML --- 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) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Proof/proofchecker.ML --- 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) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Proof/reconstruct.ML --- 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}) = diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Syntax/printer.ML --- 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 = diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/Syntax/syntax.ML --- 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); diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/codegen.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/display.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/drule.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/goals.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/meta_simplifier.ML --- 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*) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/net.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/pattern.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/proofterm.ML --- 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') => diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/search.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/sign.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/tactic.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/tctical.ML --- 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 diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/term.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/thm.ML --- 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 ***) diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/type.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/Pure/unify.ML --- 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 = diff -r cf53c2dcf440 -r b1d1b5bfc464 src/ZF/Tools/datatype_package.ML --- 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, diff -r cf53c2dcf440 -r b1d1b5bfc464 src/ZF/Tools/induct_tacs.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/ZF/Tools/inductive_package.ML --- 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; diff -r cf53c2dcf440 -r b1d1b5bfc464 src/ZF/Tools/primrec_package.ML --- 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