Removed practically all references to Library.foldr.
authorskalberg
Fri Mar 04 15:07:34 2005 +0100 (2005-03-04)
changeset 15574b1d1b5bfc464
parent 15573 cf53c2dcf440
child 15575 63babb1ee883
Removed practically all references to Library.foldr.
TFL/post.ML
TFL/rules.ML
TFL/tfl.ML
etc/settings
lib/Tools/convert
lib/Tools/expandshort
lib/Tools/fixclasimp
lib/Tools/fixdatatype
lib/Tools/fixdots
lib/Tools/fixgoal
lib/Tools/fixgreek
lib/Tools/fixseq
lib/Tools/fixsome
lib/Tools/install
lib/Tools/logo
lib/Tools/mkdir
lib/Tools/unsymbolize
src/FOLP/simp.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Import/shuffler.ML
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/presburger.ML
src/HOL/Library/EfficientNat.thy
src/HOL/Matrix/eq_codegen.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/split_rule.ML
src/HOL/ex/svc_funcs.ML
src/HOL/hologic.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/induct_method.ML
src/Provers/order.ML
src/Provers/simp.ML
src/Provers/trancl.ML
src/Provers/typedsimp.ML
src/Pure/General/lazy_seq.ML
src/Pure/General/name_space.ML
src/Pure/General/seq.ML
src/Pure/General/table.ML
src/Pure/IsaPlanner/isand.ML
src/Pure/IsaPlanner/rw_inst.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/net_rules.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/codegen.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/goals.ML
src/Pure/meta_simplifier.ML
src/Pure/net.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/search.ML
src/Pure/sign.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
src/Pure/term.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/unify.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/TFL/post.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/TFL/post.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4   *--------------------------------------------------------------------------*)
     1.5  fun termination_goals rules =
     1.6      map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
     1.7 -      (Library.foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
     1.8 +      (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
     1.9  
    1.10  (*---------------------------------------------------------------------------
    1.11   * Finds the termination conditions in (highly massaged) definition and
     2.1 --- a/TFL/rules.ML	Fri Mar 04 11:44:26 2005 +0100
     2.2 +++ b/TFL/rules.ML	Fri Mar 04 15:07:34 2005 +0100
     2.3 @@ -133,8 +133,8 @@
     2.4  
     2.5  fun FILTER_DISCH_ALL P thm =
     2.6   let fun check tm = P (#t (Thm.rep_cterm tm))
     2.7 - in  Library.foldr (fn (tm,th) => if check tm then DISCH tm th else th)
     2.8 -              (chyps thm, thm)
     2.9 + in  foldr (fn (tm,th) => if check tm then DISCH tm th else th)
    2.10 +              thm (chyps thm)
    2.11   end;
    2.12  
    2.13  (* freezeT expensive! *)
     3.1 --- a/TFL/tfl.ML	Fri Mar 04 11:44:26 2005 +0100
     3.2 +++ b/TFL/tfl.ML	Fri Mar 04 15:07:34 2005 +0100
     3.3 @@ -336,7 +336,7 @@
     3.4       val dummy = map (no_repeat_vars thy) pats
     3.5       val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
     3.6                                map (fn (t,i) => (t,(i,true))) (enumerate R))
     3.7 -     val names = Library.foldr add_term_names (R,[])
     3.8 +     val names = foldr add_term_names [] R
     3.9       val atype = type_of(hd pats)
    3.10       and aname = variant names "a"
    3.11       val a = Free(aname,atype)
    3.12 @@ -499,7 +499,7 @@
    3.13       val tych = Thry.typecheck thy
    3.14       val WFREC_THM0 = R.ISPEC (tych functional) Thms.WFREC_COROLLARY
    3.15       val Const("All",_) $ Abs(Rname,Rtype,_) = concl WFREC_THM0
    3.16 -     val R = Free (variant (Library.foldr add_term_names (eqns,[])) Rname,
    3.17 +     val R = Free (variant (foldr add_term_names [] eqns) Rname,
    3.18                     Rtype)
    3.19       val WFREC_THM = R.ISPECL [tych R, tych g] WFREC_THM0
    3.20       val ([proto_def, WFR],_) = S.strip_imp(concl WFREC_THM)
    3.21 @@ -540,7 +540,7 @@
    3.22                         prths extractants;
    3.23                         ())
    3.24                   else ()
    3.25 -     val TCs = Library.foldr (gen_union (op aconv)) (TCl, [])
    3.26 +     val TCs = foldr (gen_union (op aconv)) [] TCl
    3.27       val full_rqt = WFR::TCs
    3.28       val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
    3.29       val R'abs = S.rand R'
    3.30 @@ -698,7 +698,7 @@
    3.31   let val tych = Thry.typecheck thy
    3.32       val ty_info = Thry.induct_info thy
    3.33   in fn pats =>
    3.34 - let val names = Library.foldr add_term_names (pats,[])
    3.35 + let val names = foldr add_term_names [] pats
    3.36       val T = type_of (hd pats)
    3.37       val aname = Term.variant names "a"
    3.38       val vname = Term.variant (aname::names) "v"
    3.39 @@ -851,8 +851,8 @@
    3.40      val (pats,TCsl) = ListPair.unzip pat_TCs_list
    3.41      val case_thm = complete_cases thy pats
    3.42      val domain = (type_of o hd) pats
    3.43 -    val Pname = Term.variant (Library.foldr (Library.foldr add_term_names)
    3.44 -                              (pats::TCsl, [])) "P"
    3.45 +    val Pname = Term.variant (foldr (Library.foldr add_term_names)
    3.46 +                              [] (pats::TCsl)) "P"
    3.47      val P = Free(Pname, domain --> HOLogic.boolT)
    3.48      val Sinduct = R.SPEC (tych P) Sinduction
    3.49      val Sinduct_assumf = S.rand ((#ant o S.dest_imp o concl) Sinduct)
    3.50 @@ -862,7 +862,7 @@
    3.51      val cases = map (fn pat => betapply (Sinduct_assumf, pat)) pats
    3.52      val tasks = U.zip3 cases TCl' (R.CONJUNCTS Rinduct_assum)
    3.53      val proved_cases = map (prove_case fconst thy) tasks
    3.54 -    val v = Free (variant (Library.foldr add_term_names (map concl proved_cases, []))
    3.55 +    val v = Free (variant (foldr add_term_names [] (map concl proved_cases))
    3.56                      "v",
    3.57                    domain)
    3.58      val vtyped = tych v
     4.1 --- a/etc/settings	Fri Mar 04 11:44:26 2005 +0100
     4.2 +++ b/etc/settings	Fri Mar 04 15:07:34 2005 +0100
     4.3 @@ -46,7 +46,7 @@
     4.4  
     4.5  # Standard ML of New Jersey 110 or later
     4.6  #ML_SYSTEM=smlnj-110
     4.7 -#ML_HOME="$ISABELLE_HOME/../smlnj/bin"
     4.8 +#ML_HOME="/usr/local/smlnj/bin"
     4.9  #ML_OPTIONS="@SMLdebug=/dev/null"
    4.10  #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    4.11  
     5.1 --- a/lib/Tools/convert	Fri Mar 04 11:44:26 2005 +0100
     5.2 +++ b/lib/Tools/convert	Fri Mar 04 15:07:34 2005 +0100
     5.3 @@ -36,7 +36,7 @@
     5.4  ## main
     5.5  
     5.6  #set by configure
     5.7 -AUTO_PERL=perl
     5.8 +AUTO_PERL=/usr/bin/perl
     5.9  
    5.10  find $SPECS \( -name \*.ML \) -print | \
    5.11    xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl"
     6.1 --- a/lib/Tools/expandshort	Fri Mar 04 11:44:26 2005 +0100
     6.2 +++ b/lib/Tools/expandshort	Fri Mar 04 15:07:34 2005 +0100
     6.3 @@ -34,6 +34,6 @@
     6.4  ## main
     6.5  
     6.6  #set by configure
     6.7 -AUTO_PERL=perl
     6.8 +AUTO_PERL=/usr/bin/perl
     6.9  
    6.10  find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/expandshort.pl"
     7.1 --- a/lib/Tools/fixclasimp	Fri Mar 04 11:44:26 2005 +0100
     7.2 +++ b/lib/Tools/fixclasimp	Fri Mar 04 15:07:34 2005 +0100
     7.3 @@ -34,6 +34,6 @@
     7.4  ## main
     7.5  
     7.6  #set by configure
     7.7 -AUTO_PERL=perl
     7.8 +AUTO_PERL=/usr/bin/perl
     7.9  
    7.10  find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixclasimp.pl"
     8.1 --- a/lib/Tools/fixdatatype	Fri Mar 04 11:44:26 2005 +0100
     8.2 +++ b/lib/Tools/fixdatatype	Fri Mar 04 15:07:34 2005 +0100
     8.3 @@ -34,7 +34,7 @@
     8.4  ## main
     8.5  
     8.6  #set by configure
     8.7 -AUTO_PERL=perl
     8.8 +AUTO_PERL=/usr/bin/perl
     8.9  
    8.10  find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    8.11    xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdatatype.pl"
     9.1 --- a/lib/Tools/fixdots	Fri Mar 04 11:44:26 2005 +0100
     9.2 +++ b/lib/Tools/fixdots	Fri Mar 04 15:07:34 2005 +0100
     9.3 @@ -34,7 +34,7 @@
     9.4  ## main
     9.5  
     9.6  #set by configure
     9.7 -AUTO_PERL=perl
     9.8 +AUTO_PERL=/usr/bin/perl
     9.9  
    9.10  find $SPECS \( -name \*.thy -o -name \*.ML \) -print | \
    9.11    xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixdots.pl"
    10.1 --- a/lib/Tools/fixgoal	Fri Mar 04 11:44:26 2005 +0100
    10.2 +++ b/lib/Tools/fixgoal	Fri Mar 04 15:07:34 2005 +0100
    10.3 @@ -34,6 +34,6 @@
    10.4  ## main
    10.5  
    10.6  #set by configure
    10.7 -AUTO_PERL=perl
    10.8 +AUTO_PERL=/usr/bin/perl
    10.9  
   10.10  find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgoal.pl"
    11.1 --- a/lib/Tools/fixgreek	Fri Mar 04 11:44:26 2005 +0100
    11.2 +++ b/lib/Tools/fixgreek	Fri Mar 04 15:07:34 2005 +0100
    11.3 @@ -35,7 +35,7 @@
    11.4  ## main
    11.5  
    11.6  #set by configure
    11.7 -AUTO_PERL=perl
    11.8 +AUTO_PERL=/usr/bin/perl
    11.9  
   11.10  find $SPECS -name \*.thy -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
   11.11  find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixgreek.pl"
    12.1 --- a/lib/Tools/fixseq	Fri Mar 04 11:44:26 2005 +0100
    12.2 +++ b/lib/Tools/fixseq	Fri Mar 04 15:07:34 2005 +0100
    12.3 @@ -34,6 +34,6 @@
    12.4  ## main
    12.5  
    12.6  #set by configure
    12.7 -AUTO_PERL=perl
    12.8 +AUTO_PERL=/usr/bin/perl
    12.9  
   12.10  find $SPECS -name \*.ML -print | xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixseq.pl"
    13.1 --- a/lib/Tools/fixsome	Fri Mar 04 11:44:26 2005 +0100
    13.2 +++ b/lib/Tools/fixsome	Fri Mar 04 15:07:34 2005 +0100
    13.3 @@ -34,7 +34,7 @@
    13.4  ## main
    13.5  
    13.6  #set by configure
    13.7 -AUTO_PERL=perl
    13.8 +AUTO_PERL=/usr/bin/perl
    13.9  
   13.10  find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
   13.11    xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/fixsome.pl"
    14.1 --- a/lib/Tools/install	Fri Mar 04 11:44:26 2005 +0100
    14.2 +++ b/lib/Tools/install	Fri Mar 04 15:07:34 2005 +0100
    14.3 @@ -80,7 +80,7 @@
    14.4  # standalone binaries
    14.5  
    14.6  #set by configure
    14.7 -AUTO_BASH=bash
    14.8 +AUTO_BASH=/bin/bash
    14.9  
   14.10  case "$AUTO_BASH" in
   14.11    /*)
    15.1 --- a/lib/Tools/logo	Fri Mar 04 11:44:26 2005 +0100
    15.2 +++ b/lib/Tools/logo	Fri Mar 04 15:07:34 2005 +0100
    15.3 @@ -71,7 +71,7 @@
    15.4  fi
    15.5  
    15.6  #set by configure
    15.7 -AUTO_PERL=perl
    15.8 +AUTO_PERL=/usr/bin/perl
    15.9  
   15.10  if [ "$OUTFILE" = "-" ]; then
   15.11    "$AUTO_PERL" -p -e "s/<any>/$NAME/" "$ISABELLE_HOME/lib/logo/isabelle_any.eps"
    16.1 --- a/lib/Tools/mkdir	Fri Mar 04 11:44:26 2005 +0100
    16.2 +++ b/lib/Tools/mkdir	Fri Mar 04 15:07:34 2005 +0100
    16.3 @@ -198,7 +198,7 @@
    16.4  # document directory
    16.5  
    16.6  #set by configure
    16.7 -AUTO_PERL=perl
    16.8 +AUTO_PERL=/usr/bin/perl
    16.9  
   16.10  if [ -e document ]; then
   16.11    echo "keeping $PREFIX/document" >&2
    17.1 --- a/lib/Tools/unsymbolize	Fri Mar 04 11:44:26 2005 +0100
    17.2 +++ b/lib/Tools/unsymbolize	Fri Mar 04 15:07:34 2005 +0100
    17.3 @@ -35,7 +35,7 @@
    17.4  ## main
    17.5  
    17.6  #set by configure
    17.7 -AUTO_PERL=perl
    17.8 +AUTO_PERL=/usr/bin/perl
    17.9  
   17.10  find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \
   17.11    xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/unsymbolize.pl"
    18.1 --- a/src/FOLP/simp.ML	Fri Mar 04 11:44:26 2005 +0100
    18.2 +++ b/src/FOLP/simp.ML	Fri Mar 04 15:07:34 2005 +0100
    18.3 @@ -161,7 +161,7 @@
    18.4                       in case f of
    18.5                              Const(c,T) => 
    18.6                                  if c mem ccs
    18.7 -                                then Library.foldr add_hvars (args,hvars)
    18.8 +                                then foldr add_hvars hvars args
    18.9                                  else add_term_vars(tm,hvars)
   18.10                            | _ => add_term_vars(tm,hvars)
   18.11                       end
   18.12 @@ -173,7 +173,7 @@
   18.13                  if at then vars else add_term_vars(tm,vars)
   18.14          fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
   18.15                  in if length(tml)=length(al)
   18.16 -                   then Library.foldr itf (tml~~al,vars)
   18.17 +                   then foldr itf vars (tml~~al)
   18.18                     else vars
   18.19                  end
   18.20          fun add_vars (tm,vars) = case tm of
   18.21 @@ -194,12 +194,12 @@
   18.22      val lhs = rhs_of_eq 1 thm'
   18.23      val rhs = lhs_of_eq nops thm'
   18.24      val asms = tl(rev(tl(prems_of thm')))
   18.25 -    val hvars = Library.foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
   18.26 +    val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms)
   18.27      val hvars = add_new_asm_vars new_asms (rhs,hvars)
   18.28      fun it_asms (asm,hvars) =
   18.29          if atomic asm then add_new_asm_vars new_asms (asm,hvars)
   18.30          else add_term_frees(asm,hvars)
   18.31 -    val hvars = Library.foldr it_asms (asms,hvars)
   18.32 +    val hvars = foldr it_asms hvars asms
   18.33      val hvs = map (#1 o dest_Var) hvars
   18.34      val refl1_tac = refl_tac 1
   18.35      fun norm_step_tac st = st |>
   18.36 @@ -252,12 +252,12 @@
   18.37      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
   18.38       net);
   18.39  
   18.40 -val insert_thms = Library.foldr insert_thm_warn;
   18.41 +val insert_thms = foldr insert_thm_warn;
   18.42  
   18.43  fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
   18.44  let val thms = mk_simps thm
   18.45  in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
   18.46 -      simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net)}
   18.47 +      simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms}
   18.48  end;
   18.49  
   18.50  val op addrews = Library.foldl addrew;
   18.51 @@ -265,7 +265,7 @@
   18.52  fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
   18.53  let val congs' = thms @ congs;
   18.54  in SS{auto_tac=auto_tac, congs= congs',
   18.55 -      cong_net= insert_thms (map mk_trans thms,cong_net),
   18.56 +      cong_net= insert_thms cong_net (map mk_trans thms),
   18.57        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
   18.58  end;
   18.59  
   18.60 @@ -278,12 +278,12 @@
   18.61      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
   18.62       net);
   18.63  
   18.64 -val delete_thms = Library.foldr delete_thm_warn;
   18.65 +val delete_thms = foldr delete_thm_warn;
   18.66  
   18.67  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
   18.68  let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
   18.69  in SS{auto_tac=auto_tac, congs= congs',
   18.70 -      cong_net= delete_thms(map mk_trans thms,cong_net),
   18.71 +      cong_net= delete_thms cong_net (map mk_trans thms),
   18.72        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
   18.73  end;
   18.74  
   18.75 @@ -295,7 +295,7 @@
   18.76                             ([],simps'))
   18.77      val (thms,simps') = find(simps,[])
   18.78  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
   18.79 -      simps = simps', simp_net = delete_thms(thms,simp_net)}
   18.80 +      simps = simps', simp_net = delete_thms simp_net thms}
   18.81  end;
   18.82  
   18.83  val op delrews = Library.foldl delrew;
   18.84 @@ -439,7 +439,7 @@
   18.85          val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
   18.86          val new_rws = List.concat(map mk_rew_rules thms);
   18.87          val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
   18.88 -        val anet' = Library.foldr lhs_insert_thm (rwrls,anet)
   18.89 +        val anet' = foldr lhs_insert_thm anet rwrls
   18.90      in  if !tracing andalso not(null new_rws)
   18.91          then (writeln"Adding rewrites:";  prths new_rws;  ())
   18.92          else ();
    19.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Mar 04 11:44:26 2005 +0100
    19.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Mar 04 15:07:34 2005 +0100
    19.3 @@ -675,7 +675,7 @@
    19.4  		val (c,asl) = case terms of
    19.5  				  [] => raise ERR "x2p" "Bad oracle description"
    19.6  				| (hd::tl) => (hd,tl)
    19.7 -		val tg = Library.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) (ors,Tag.empty_tag)
    19.8 +		val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors
    19.9  	    in
   19.10  		mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c))
   19.11  	    end
   19.12 @@ -1064,7 +1064,7 @@
   19.13  	  | process _ = raise ERR "disamb_helper" "Internal error"
   19.14  
   19.15  	val (vars',rens',inst) =
   19.16 -	    Library.foldr process (varstm,(vars,rens,[]))
   19.17 +	    foldr process (vars,rens,[]) varstm
   19.18      in
   19.19  	({vars=vars',rens=rens'},inst)
   19.20      end
   19.21 @@ -1100,22 +1100,22 @@
   19.22      end
   19.23  
   19.24  fun disamb_terms_from info tms =
   19.25 -    Library.foldr (fn (tm,(info,tms)) =>
   19.26 +    foldr (fn (tm,(info,tms)) =>
   19.27  	      let
   19.28  		  val (info',tm') = disamb_term_from info tm
   19.29  	      in
   19.30  		  (info',tm'::tms)
   19.31  	      end)
   19.32 -	  (tms,(info,[]))
   19.33 +	  (info,[]) tms
   19.34  
   19.35  fun disamb_thms_from info hthms =
   19.36 -    Library.foldr (fn (hthm,(info,thms)) =>
   19.37 +    foldr (fn (hthm,(info,thms)) =>
   19.38  	      let
   19.39  		  val (info',tm') = disamb_thm_from info hthm
   19.40  	      in
   19.41  		  (info',tm'::thms)
   19.42  	      end)
   19.43 -	  (hthms,(info,[]))
   19.44 +	  (info,[]) hthms
   19.45  
   19.46  fun disamb_term tm   = disamb_term_from disamb_info_empty tm
   19.47  fun disamb_terms tms = disamb_terms_from disamb_info_empty tms
   19.48 @@ -1127,7 +1127,7 @@
   19.49      let
   19.50  	val vars = collect_vars (prop_of th)
   19.51  	val (rens',inst,_) =
   19.52 -	    Library.foldr (fn((ren as (vold as Free(vname,_),vnew)),
   19.53 +	    foldr (fn((ren as (vold as Free(vname,_),vnew)),
   19.54  		      (rens,inst,vars)) =>
   19.55  		     (case Library.find_first (fn Free(v,_) => v = vname | _ => false) vars of
   19.56  			  SOME v' => if v' = vold
   19.57 @@ -1135,7 +1135,7 @@
   19.58  				     else (ren::rens,(vold,vnew)::inst,vnew::vars)
   19.59  			| NONE => (rens,(vnew,vold)::inst,vold::vars))
   19.60  		   | _ => raise ERR "norm_hthm" "Internal error")
   19.61 -		  (rens,([],[],vars))
   19.62 +		  ([],[],vars) rens
   19.63  	val (dom,rng) = ListPair.unzip inst
   19.64  	val th' = mk_INST (map (cterm_of sg) dom) (map (cterm_of sg) rng) th
   19.65  	val nvars = collect_vars (prop_of th')
   19.66 @@ -1794,7 +1794,7 @@
   19.67  		      | inst_type ty1 ty2 (ty as Type(name,tys)) =
   19.68  			Type(name,map (inst_type ty1 ty2) tys)
   19.69  		in
   19.70 -		    Library.foldr (fn (v,th) =>
   19.71 +		    foldr (fn (v,th) =>
   19.72  			      let
   19.73  				  val cdom = fst (dom_rng (fst (dom_rng cty)))
   19.74  				  val vty  = type_of v
   19.75 @@ -1802,11 +1802,11 @@
   19.76  				  val cc = cterm_of sg (Const(cname,newcty))
   19.77  			      in
   19.78  				  mk_COMB (mk_REFL cc) (mk_ABS v th sg) sg
   19.79 -			      end) (vlist',th)
   19.80 +			      end) th vlist'
   19.81  		end
   19.82  	      | SOME _ => raise ERR "GEN_ABS" "Bad constant"
   19.83  	      | NONE => 
   19.84 -		Library.foldr (fn (v,th) => mk_ABS v th sg) (vlist',th)
   19.85 +		foldr (fn (v,th) => mk_ABS v th sg) th vlist'
   19.86  	val res = HOLThm(rens_of info',th1)
   19.87  	val _ = message "RESULT:"
   19.88  	val _ = if_debug pth res
   19.89 @@ -1970,8 +1970,8 @@
   19.90  			       Theory.add_consts_i consts thy'
   19.91  			   end
   19.92  
   19.93 -	    val thy1 = Library.foldr (fn(name,thy)=>
   19.94 -				snd (get_defname thyname name thy)) (names,thy1)
   19.95 +	    val thy1 = foldr (fn(name,thy)=>
   19.96 +				snd (get_defname thyname name thy)) thy1 names
   19.97  	    fun new_name name = fst (get_defname thyname name thy1)
   19.98  	    val (thy',res) = SpecificationPackage.add_specification_i NONE
   19.99  				 (map (fn name => (new_name name,name,false)) names)
  19.100 @@ -1989,12 +1989,12 @@
  19.101  		     then quotename name
  19.102  		     else (quotename newname) ^ ": " ^ (quotename name),thy')
  19.103  		end
  19.104 -	    val (new_names,thy') = Library.foldr (fn(name,(names,thy)) =>
  19.105 +	    val (new_names,thy') = foldr (fn(name,(names,thy)) =>
  19.106  					    let
  19.107  						val (name',thy') = handle_const (name,thy)
  19.108  					    in
  19.109  						(name'::names,thy')
  19.110 -					    end) (names,([],thy'))
  19.111 +					    end) ([],thy') names
  19.112  	    val thy'' = add_dump ("specification (" ^ (spaces new_names) ^ ") " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^
  19.113  				  "\n  by (import " ^ thyname ^ " " ^ thmname ^ ")")
  19.114  				 thy'
    20.1 --- a/src/HOL/Import/replay.ML	Fri Mar 04 11:44:26 2005 +0100
    20.2 +++ b/src/HOL/Import/replay.ML	Fri Mar 04 15:07:34 2005 +0100
    20.3 @@ -25,12 +25,12 @@
    20.4  	    end
    20.5  	  | rp (PSubst(prfs,ctxt,prf)) thy =
    20.6  	    let
    20.7 -		val (thy',ths) = Library.foldr (fn (p,(thy,ths)) =>
    20.8 +		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
    20.9  					   let
   20.10  					       val (thy',th) = rp' p thy
   20.11  					   in
   20.12  					       (thy',th::ths)
   20.13 -					   end) (prfs,(thy,[]))
   20.14 +					   end) (thy,[]) prfs
   20.15  		val (thy'',th) = rp' prf thy'
   20.16  	    in
   20.17  		P.SUBST ths ctxt th thy''
    21.1 --- a/src/HOL/Import/shuffler.ML	Fri Mar 04 11:44:26 2005 +0100
    21.2 +++ b/src/HOL/Import/shuffler.ML	Fri Mar 04 15:07:34 2005 +0100
    21.3 @@ -553,13 +553,13 @@
    21.4      end
    21.5      
    21.6  val collect_ignored =
    21.7 -    Library.foldr (fn (thm,cs) =>
    21.8 +    foldr (fn (thm,cs) =>
    21.9  	      let
   21.10  		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
   21.11  		  val ignore_lhs = term_consts lhs \\ term_consts rhs
   21.12  		  val ignore_rhs = term_consts rhs \\ term_consts lhs
   21.13  	      in
   21.14 -		  Library.foldr (op ins_string) (ignore_lhs @ ignore_rhs,cs)
   21.15 +		  foldr (op ins_string) cs (ignore_lhs @ ignore_rhs)
   21.16  	      end)
   21.17  
   21.18  (* set_prop t thms tries to make a theorem with the proposition t from
   21.19 @@ -570,8 +570,8 @@
   21.20      let
   21.21  	val sg = sign_of thy
   21.22  	val vars = add_term_frees (t,add_term_vars (t,[]))
   21.23 -	val closed_t = Library.foldr (fn (v,body) => let val vT = type_of v
   21.24 -					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) (vars,t)
   21.25 +	val closed_t = foldr (fn (v,body) => let val vT = type_of v
   21.26 +					     in all vT $ (Abs("x",vT,abstract_over(v,body))) end) t vars
   21.27  	val rew_th = norm_term thy closed_t
   21.28  	val rhs = snd (dest_equals (cprop_of rew_th))
   21.29  
   21.30 @@ -610,7 +610,7 @@
   21.31  fun find_potential thy t =
   21.32      let
   21.33  	val shuffles = ShuffleData.get thy
   21.34 -	val ignored = collect_ignored(shuffles,[])
   21.35 +	val ignored = collect_ignored [] shuffles
   21.36  	val rel_consts = term_consts t \\ ignored
   21.37  	val pot_thms = PureThy.thms_containing_consts thy rel_consts
   21.38      in
    22.1 --- a/src/HOL/Integ/cooper_dec.ML	Fri Mar 04 11:44:26 2005 +0100
    22.2 +++ b/src/HOL/Integ/cooper_dec.ML	Fri Mar 04 15:07:34 2005 +0100
    22.3 @@ -442,7 +442,7 @@
    22.4     val ts = coeffs_of t
    22.5     in case ts of
    22.6       [] => raise DVD_UNKNOWN
    22.7 -    |_  => Library.foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
    22.8 +    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
    22.9     end;
   22.10  
   22.11  
   22.12 @@ -736,7 +736,7 @@
   22.13               in (rw,HOLogic.mk_disj(F',rf)) 
   22.14  	     end)
   22.15      val f = if b then linear_add else linear_sub
   22.16 -    val p_elements = Library.foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
   22.17 +    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (1 upto d)
   22.18      in h p_elements
   22.19      end;
   22.20  
    23.1 --- a/src/HOL/Integ/presburger.ML	Fri Mar 04 11:44:26 2005 +0100
    23.2 +++ b/src/HOL/Integ/presburger.ML	Fri Mar 04 15:07:34 2005 +0100
    23.3 @@ -162,10 +162,10 @@
    23.4  
    23.5  
    23.6  fun abstract_pres sg fm = 
    23.7 -  Library.foldr (fn (t, u) =>
    23.8 +  foldr (fn (t, u) =>
    23.9        let val T = fastype_of t
   23.10        in all T $ Abs ("x", T, abstract_over (t, u)) end)
   23.11 -         (getfuncs fm, fm);
   23.12 +         fm (getfuncs fm);
   23.13  
   23.14  
   23.15  
   23.16 @@ -219,11 +219,11 @@
   23.17      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
   23.18      val (rhs,irhs) = List.partition (relevant (rev ps)) hs
   23.19      val np = length ps
   23.20 -    val (fm',np) =  Library.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   23.21 -      (ps,(Library.foldr HOLogic.mk_imp (rhs, c), np))
   23.22 +    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   23.23 +      (foldr HOLogic.mk_imp c rhs, np) ps
   23.24      val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
   23.25        (term_frees fm' @ term_vars fm');
   23.26 -    val fm2 = Library.foldr mk_all2 (vs, fm')
   23.27 +    val fm2 = foldr mk_all2 fm' vs
   23.28    in (fm2, np + length vs, length rhs) end;
   23.29  
   23.30  (*Object quantifier to meta --*)
    24.1 --- a/src/HOL/Library/EfficientNat.thy	Fri Mar 04 11:44:26 2005 +0100
    24.2 +++ b/src/HOL/Library/EfficientNat.thy	Fri Mar 04 15:07:34 2005 +0100
    24.3 @@ -191,8 +191,8 @@
    24.4    let val dest = fst o HOLogic.dest_mem o HOLogic.dest_Trueprop
    24.5    in
    24.6      if forall (can (dest o concl_of)) ths andalso
    24.7 -      exists (fn th => "Suc" mem Library.foldr add_term_consts
    24.8 -        (List.mapPartial (try dest) (concl_of th :: prems_of th), [])) ths
    24.9 +      exists (fn th => "Suc" mem foldr add_term_consts
   24.10 +        [] (List.mapPartial (try dest) (concl_of th :: prems_of th))) ths
   24.11      then remove_suc_clause thy ths else ths
   24.12    end;
   24.13  
    25.1 --- a/src/HOL/Matrix/eq_codegen.ML	Fri Mar 04 11:44:26 2005 +0100
    25.2 +++ b/src/HOL/Matrix/eq_codegen.ML	Fri Mar 04 15:07:34 2005 +0100
    25.3 @@ -377,8 +377,8 @@
    25.4        | SOME thms => SOME (unsuffix "_case" (Sign.base_name s) ^ ".cases",
    25.5            map (fn i => Sign.base_name s ^ "_" ^ string_of_int i)
    25.6              (1 upto length thms) ~~ thms)))
    25.7 -      (Library.foldr add_term_consts (map (prop_of o snd)
    25.8 -        (List.concat (map (#3 o snd) fs')), []));
    25.9 +      (foldr add_term_consts [] (map (prop_of o snd)
   25.10 +        (List.concat (map (#3 o snd) fs'))));
   25.11      val case_vals = map (fn (s, cs) => mk_vall (map fst cs)
   25.12        [Pretty.str "map my_mk_meta_eq", Pretty.brk 1,
   25.13         Pretty.str ("(thms \"" ^ s ^ "\")")]) case_thms;
   25.14 @@ -460,10 +460,10 @@
   25.15      fun mk_edges (s, _, ths) = map (pair s) (distinct
   25.16        (List.mapPartial (fn t => Option.map #1 (lookup sg eqns' t))
   25.17          (List.concat (map (term_consts' o prop_of o snd) ths))));
   25.18 -    val gr = Library.foldr (uncurry Graph.add_edge)
   25.19 -      (map (pair "" o #1) eqns @ List.concat (map mk_edges eqns),
   25.20 -       Library.foldr (uncurry Graph.new_node)
   25.21 -         (("", Bound 0) :: map mk_node eqns, Graph.empty));
   25.22 +    val gr = foldr (uncurry Graph.add_edge)
   25.23 +      (Library.foldr (uncurry Graph.new_node)
   25.24 +         (("", Bound 0) :: map mk_node eqns, Graph.empty))
   25.25 +      (map (pair "" o #1) eqns @ List.concat (map mk_edges eqns));
   25.26      val keys = rev (Graph.all_succs gr [""] \ "");
   25.27      fun gr_ord (x :: _, y :: _) =
   25.28        int_ord (find_index (equal x) keys, find_index (equal y) keys);
    26.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Fri Mar 04 11:44:26 2005 +0100
    26.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Fri Mar 04 15:07:34 2005 +0100
    26.3 @@ -253,7 +253,7 @@
    26.4        fun newName (Var(ix,_), (pairs,used)) = 
    26.5            let val v = variant used (string_of_indexname ix)
    26.6            in  ((ix,v)::pairs, v::used)  end;
    26.7 -      val (alist, _) = Library.foldr newName (vars, ([], used));
    26.8 +      val (alist, _) = foldr newName ([], used) vars;
    26.9        fun mk_inst (Var(v,T)) = 
   26.10            (Var(v,T),
   26.11             Free(valOf (assoc(alist,v)), T));
    27.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Mar 04 11:44:26 2005 +0100
    27.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Fri Mar 04 15:07:34 2005 +0100
    27.3 @@ -442,7 +442,7 @@
    27.4     val ts = coeffs_of t
    27.5     in case ts of
    27.6       [] => raise DVD_UNKNOWN
    27.7 -    |_  => Library.foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
    27.8 +    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) true ts
    27.9     end;
   27.10  
   27.11  
   27.12 @@ -736,7 +736,7 @@
   27.13               in (rw,HOLogic.mk_disj(F',rf)) 
   27.14  	     end)
   27.15      val f = if b then linear_add else linear_sub
   27.16 -    val p_elements = Library.foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
   27.17 +    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) [] (1 upto d)
   27.18      in h p_elements
   27.19      end;
   27.20  
    28.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 04 11:44:26 2005 +0100
    28.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 04 15:07:34 2005 +0100
    28.3 @@ -162,10 +162,10 @@
    28.4  
    28.5  
    28.6  fun abstract_pres sg fm = 
    28.7 -  Library.foldr (fn (t, u) =>
    28.8 +  foldr (fn (t, u) =>
    28.9        let val T = fastype_of t
   28.10        in all T $ Abs ("x", T, abstract_over (t, u)) end)
   28.11 -         (getfuncs fm, fm);
   28.12 +         fm (getfuncs fm);
   28.13  
   28.14  
   28.15  
   28.16 @@ -219,11 +219,11 @@
   28.17      fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;
   28.18      val (rhs,irhs) = List.partition (relevant (rev ps)) hs
   28.19      val np = length ps
   28.20 -    val (fm',np) =  Library.foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   28.21 -      (ps,(Library.foldr HOLogic.mk_imp (rhs, c), np))
   28.22 +    val (fm',np) =  foldr (fn ((x, T), (fm,n)) => mk_all ((x, T), (fm,n)))
   28.23 +      (foldr HOLogic.mk_imp c rhs, np) ps
   28.24      val (vs, _) = List.partition (fn t => q orelse (type_of t) = nT)
   28.25        (term_frees fm' @ term_vars fm');
   28.26 -    val fm2 = Library.foldr mk_all2 (vs, fm')
   28.27 +    val fm2 = foldr mk_all2 fm' vs
   28.28    in (fm2, np + length vs, length rhs) end;
   28.29  
   28.30  (*Object quantifier to meta --*)
    29.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Mar 04 11:44:26 2005 +0100
    29.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Mar 04 15:07:34 2005 +0100
    29.3 @@ -97,7 +97,7 @@
    29.4  
    29.5      val descr' = List.concat descr;
    29.6      val recTs = get_rec_types descr' sorts;
    29.7 -    val used = Library.foldr add_typ_tfree_names (recTs, []);
    29.8 +    val used = foldr add_typ_tfree_names [] recTs;
    29.9      val newTs = Library.take (length (hd descr), recTs);
   29.10  
   29.11      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
   29.12 @@ -139,7 +139,7 @@
   29.13            end;
   29.14  
   29.15          val Ts = map (typ_of_dtyp descr' sorts) cargs;
   29.16 -        val (_, _, prems, t1s, t2s) = Library.foldr mk_prem (cargs ~~ Ts, (1, 1, [], [], []))
   29.17 +        val (_, _, prems, t1s, t2s) = foldr mk_prem (1, 1, [], [], []) (cargs ~~ Ts)
   29.18  
   29.19        in (rec_intr_ts @ [Logic.list_implies (prems, HOLogic.mk_Trueprop (HOLogic.mk_mem
   29.20          (HOLogic.mk_prod (list_comb (Const (cname, Ts ---> T), t1s),
   29.21 @@ -269,7 +269,7 @@
   29.22  
   29.23      val descr' = List.concat descr;
   29.24      val recTs = get_rec_types descr' sorts;
   29.25 -    val used = Library.foldr add_typ_tfree_names (recTs, []);
   29.26 +    val used = foldr add_typ_tfree_names [] recTs;
   29.27      val newTs = Library.take (length (hd descr), recTs);
   29.28      val T' = TFree (variant used "'t", HOLogic.typeS);
   29.29  
   29.30 @@ -401,7 +401,7 @@
   29.31          val t = if k = 0 then HOLogic.zero else
   29.32            foldl1 plus (map Bound (k - 1 downto 0) @ [HOLogic.mk_nat 1])
   29.33        in
   29.34 -        Library.foldr (fn (T, t') => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT, t)
   29.35 +        foldr (fn (T, t') => Abs ("x", T, t')) t (Ts @ replicate k HOLogic.natT)
   29.36        end;
   29.37  
   29.38      val fs = List.concat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
    30.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Mar 04 11:44:26 2005 +0100
    30.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Mar 04 15:07:34 2005 +0100
    30.3 @@ -155,8 +155,8 @@
    30.4      val prem' = hd (prems_of exhaustion);
    30.5      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
    30.6      val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
    30.7 -      cterm_of sg (Library.foldr (fn ((_, T), t) => Abs ("z", T, t))
    30.8 -        (params, Bound 0)))] exhaustion
    30.9 +      cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
   30.10 +        (Bound 0) params))] exhaustion
   30.11    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
   30.12    end;
   30.13  
   30.14 @@ -265,8 +265,8 @@
   30.15  
   30.16  fun get_branching_types descr sorts =
   30.17    map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
   30.18 -    Library.foldl (fn (Ts', (_, cargs)) => Library.foldr op union (map (fst o strip_dtyp)
   30.19 -      cargs, Ts')) (Ts, constrs)) ([], descr));
   30.20 +    Library.foldl (fn (Ts', (_, cargs)) => foldr op union Ts' (map (fst o strip_dtyp)
   30.21 +      cargs)) (Ts, constrs)) ([], descr));
   30.22  
   30.23  fun get_arities descr = Library.foldl (fn (is, (_, (_, _, constrs))) =>
   30.24    Library.foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)
    31.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Mar 04 11:44:26 2005 +0100
    31.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Mar 04 15:07:34 2005 +0100
    31.3 @@ -201,8 +201,8 @@
    31.4        let
    31.5          val ts1 = Library.take (i, ts);
    31.6          val t :: ts2 = Library.drop (i, ts);
    31.7 -        val names = Library.foldr add_term_names (ts1,
    31.8 -          map (fst o fst o dest_Var) (Library.foldr add_term_vars (ts1, [])));
    31.9 +        val names = foldr add_term_names
   31.10 +          (map (fst o fst o dest_Var) (foldr add_term_vars [] ts1)) ts1;
   31.11          val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
   31.12  
   31.13          fun pcase gr [] [] [] = ([], gr)
    32.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Mar 04 11:44:26 2005 +0100
    32.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Mar 04 15:07:34 2005 +0100
    32.3 @@ -169,7 +169,7 @@
    32.4  fun occs_in_prems tacf vars =
    32.5    SUBGOAL (fn (Bi, i) =>
    32.6             (if  exists (fn Free (a, _) => a mem vars)
    32.7 -                      (Library.foldr add_term_frees (#2 (strip_context Bi), []))
    32.8 +                      (foldr add_term_frees [] (#2 (strip_context Bi)))
    32.9               then warning "Induction variable occurs also among premises!"
   32.10               else ();
   32.11              tacf i));
   32.12 @@ -431,7 +431,7 @@
   32.13                   if length dt <> length vs then
   32.14                      case_error ("Wrong number of arguments for constructor " ^ s)
   32.15                        (SOME tname) vs
   32.16 -                 else (cases \ c, Library.foldr abstr (vs, t)))
   32.17 +                 else (cases \ c, foldr abstr t vs))
   32.18            val (cases'', fs) = foldl_map find_case (cases', constrs)
   32.19          in case (cases'', length constrs = length cases', default) of
   32.20              ([], true, SOME _) =>
   32.21 @@ -542,32 +542,32 @@
   32.22  (********************* axiomatic introduction of datatypes ********************)
   32.23  
   32.24  fun add_and_get_axioms_atts label tnames attss ts thy =
   32.25 -  Library.foldr (fn (((tname, atts), t), (thy', axs)) =>
   32.26 +  foldr (fn (((tname, atts), t), (thy', axs)) =>
   32.27      let
   32.28        val (thy'', [ax]) = thy' |>
   32.29          Theory.add_path tname |>
   32.30          PureThy.add_axioms_i [((label, t), atts)];
   32.31      in (Theory.parent_path thy'', ax::axs)
   32.32 -    end) (tnames ~~ attss ~~ ts, (thy, []));
   32.33 +    end) (thy, []) (tnames ~~ attss ~~ ts);
   32.34  
   32.35  fun add_and_get_axioms label tnames =
   32.36    add_and_get_axioms_atts label tnames (replicate (length tnames) []);
   32.37  
   32.38  fun add_and_get_axiomss label tnames tss thy =
   32.39 -  Library.foldr (fn ((tname, ts), (thy', axss)) =>
   32.40 +  foldr (fn ((tname, ts), (thy', axss)) =>
   32.41      let
   32.42        val (thy'', [axs]) = thy' |>
   32.43          Theory.add_path tname |>
   32.44          PureThy.add_axiomss_i [((label, ts), [])];
   32.45      in (Theory.parent_path thy'', axs::axss)
   32.46 -    end) (tnames ~~ tss, (thy, []));
   32.47 +    end) (thy, []) (tnames ~~ tss);
   32.48  
   32.49  fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   32.50      case_names_induct case_names_exhausts thy =
   32.51    let
   32.52      val descr' = List.concat descr;
   32.53      val recTs = get_rec_types descr' sorts;
   32.54 -    val used = Library.foldr add_typ_tfree_names (recTs, []);
   32.55 +    val used = foldr add_typ_tfree_names [] recTs;
   32.56      val newTs = Library.take (length (hd descr), recTs);
   32.57  
   32.58      val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
   32.59 @@ -694,7 +694,7 @@
   32.60        Theory.add_path (space_implode "_" new_type_names) |>
   32.61        add_rules simps case_thms size_thms rec_thms inject distinct
   32.62                  weak_case_congs Simplifier.cong_add_global |> 
   32.63 -      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
   32.64 +      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
   32.65        add_cases_induct dt_infos induct |>
   32.66        Theory.parent_path |>
   32.67        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   32.68 @@ -752,7 +752,7 @@
   32.69        Theory.add_path (space_implode "_" new_type_names) |>
   32.70        add_rules simps case_thms size_thms rec_thms inject distinct
   32.71                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
   32.72 -      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
   32.73 +      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
   32.74        add_cases_induct dt_infos induct |>
   32.75        Theory.parent_path |>
   32.76        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   32.77 @@ -860,7 +860,7 @@
   32.78        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
   32.79        add_rules simps case_thms size_thms rec_thms inject distinct
   32.80                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
   32.81 -      put_datatypes (Library.foldr Symtab.update (dt_infos, dt_info)) |>
   32.82 +      put_datatypes (foldr Symtab.update dt_info dt_infos) |>
   32.83        add_cases_induct dt_infos induction' |>
   32.84        Theory.parent_path |>
   32.85        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   32.86 @@ -916,7 +916,7 @@
   32.87          fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
   32.88            let
   32.89              val (cargs', sorts'') = Library.foldl (prep_typ sign) (([], sorts'), cargs);
   32.90 -            val _ = (case Library.foldr add_typ_tfree_names (cargs', []) \\ tvs of
   32.91 +            val _ = (case foldr add_typ_tfree_names [] cargs' \\ tvs of
   32.92                  [] => ()
   32.93                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   32.94            in (constrs @ [((if flat_names then Sign.full_name sign else
    33.1 --- a/src/HOL/Tools/datatype_prop.ML	Fri Mar 04 11:44:26 2005 +0100
    33.2 +++ b/src/HOL/Tools/datatype_prop.ML	Fri Mar 04 15:07:34 2005 +0100
    33.3 @@ -80,7 +80,7 @@
    33.4               (map HOLogic.mk_eq (frees ~~ frees')))))::injs
    33.5          end;
    33.6  
    33.7 -  in map (fn (d, T) => Library.foldr (make_inj T) (#3 (snd d), []))
    33.8 +  in map (fn (d, T) => foldr (make_inj T) [] (#3 (snd d)))
    33.9      ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
   33.10    end;
   33.11  
   33.12 @@ -182,7 +182,7 @@
   33.13  
   33.14      val descr' = List.concat descr;
   33.15      val recTs = get_rec_types descr' sorts;
   33.16 -    val used = Library.foldr add_typ_tfree_names (recTs, []);
   33.17 +    val used = foldr add_typ_tfree_names [] recTs;
   33.18  
   33.19      val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
   33.20  
   33.21 @@ -232,7 +232,7 @@
   33.22    let
   33.23      val descr' = List.concat descr;
   33.24      val recTs = get_rec_types descr' sorts;
   33.25 -    val used = Library.foldr add_typ_tfree_names (recTs, []);
   33.26 +    val used = foldr add_typ_tfree_names [] recTs;
   33.27      val newTs = Library.take (length (hd descr), recTs);
   33.28      val T' = TFree (variant used "'t", HOLogic.typeS);
   33.29  
   33.30 @@ -317,7 +317,7 @@
   33.31    let
   33.32      val descr' = List.concat descr;
   33.33      val recTs = get_rec_types descr' sorts;
   33.34 -    val used' = Library.foldr add_typ_tfree_names (recTs, []);
   33.35 +    val used' = foldr add_typ_tfree_names [] recTs;
   33.36      val newTs = Library.take (length (hd descr), recTs);
   33.37      val T' = TFree (variant used' "'t", HOLogic.typeS);
   33.38      val P = Free ("P", T' --> HOLogic.boolT);
   33.39 @@ -334,13 +334,13 @@
   33.40              val eqn = HOLogic.mk_eq (Free ("x", T),
   33.41                list_comb (Const (cname, Ts ---> T), frees));
   33.42              val P' = P $ list_comb (f, frees)
   33.43 -          in ((Library.foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
   33.44 -                (frees, HOLogic.imp $ eqn $ P'))::t1s,
   33.45 -              (Library.foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
   33.46 -                (frees, HOLogic.conj $ eqn $ (HOLogic.Not $ P')))::t2s)
   33.47 +          in ((foldr (fn (Free (s, T), t) => HOLogic.mk_all (s, T, t))
   33.48 +                (HOLogic.imp $ eqn $ P') frees)::t1s,
   33.49 +              (foldr (fn (Free (s, T), t) => HOLogic.mk_exists (s, T, t))
   33.50 +                (HOLogic.conj $ eqn $ (HOLogic.Not $ P')) frees)::t2s)
   33.51            end;
   33.52  
   33.53 -        val (t1s, t2s) = Library.foldr process_constr (constrs ~~ fs, ([], []));
   33.54 +        val (t1s, t2s) = foldr process_constr ([], []) (constrs ~~ fs);
   33.55          val lhs = P $ (comb_t $ Free ("x", T))
   33.56        in
   33.57          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, mk_conj t1s)),
   33.58 @@ -475,9 +475,9 @@
   33.59          val tnames = variantlist (make_tnames Ts, ["v"]);
   33.60          val frees = tnames ~~ Ts
   33.61        in
   33.62 -        Library.foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
   33.63 -          (frees, HOLogic.mk_eq (Free ("v", T),
   33.64 -            list_comb (Const (cname, Ts ---> T), map Free frees)))
   33.65 +        foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
   33.66 +          (HOLogic.mk_eq (Free ("v", T),
   33.67 +            list_comb (Const (cname, Ts ---> T), map Free frees))) frees
   33.68        end
   33.69  
   33.70    in map (fn ((_, (_, _, constrs)), T) =>
    34.1 --- a/src/HOL/Tools/datatype_realizer.ML	Fri Mar 04 11:44:26 2005 +0100
    34.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 04 15:07:34 2005 +0100
    34.3 @@ -144,8 +144,8 @@
    34.4        tname_of (body_type T) mem ["set", "bool"]) ivs);
    34.5      val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (assoc (rvs, ixn)))) ivs;
    34.6  
    34.7 -    val prf = Library.foldr forall_intr_prf (ivs2,
    34.8 -      Library.foldr (fn ((f, p), prf) =>
    34.9 +    val prf = foldr forall_intr_prf
   34.10 +     (foldr (fn ((f, p), prf) =>
   34.11          (case head_of (strip_abs_body f) of
   34.12             Free (s, T) =>
   34.13               let val T' = Type.varifyT T
   34.14 @@ -153,12 +153,12 @@
   34.15                 (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
   34.16               end
   34.17           | _ => AbsP ("H", SOME p, prf)))
   34.18 -           (rec_fns ~~ prems_of thm, Proofterm.proof_combP
   34.19 -             (prf_of thm', map PBound (length prems - 1 downto 0))));
   34.20 +           (Proofterm.proof_combP
   34.21 +             (prf_of thm', map PBound (length prems - 1 downto 0))) (rec_fns ~~ prems_of thm)) ivs2;
   34.22  
   34.23 -    val r' = if null is then r else Logic.varify (Library.foldr (uncurry lambda)
   34.24 -      (map Logic.unvarify ivs1 @ filter_out is_unit
   34.25 -        (map (head_of o strip_abs_body) rec_fns), r));
   34.26 +    val r' = if null is then r else Logic.varify (foldr (uncurry lambda)
   34.27 +      r (map Logic.unvarify ivs1 @ filter_out is_unit
   34.28 +          (map (head_of o strip_abs_body) rec_fns)));
   34.29  
   34.30    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
   34.31  
   34.32 @@ -209,10 +209,10 @@
   34.33  
   34.34      val P = Var (("P", 0), rT' --> HOLogic.boolT);
   34.35      val prf = forall_intr_prf (y, forall_intr_prf (P,
   34.36 -      Library.foldr (fn ((p, r), prf) =>
   34.37 +      foldr (fn ((p, r), prf) =>
   34.38          forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
   34.39 -          prf))) (prems ~~ rs, Proofterm.proof_combP (prf_of thm',
   34.40 -            map PBound (length prems - 1 downto 0)))));
   34.41 +          prf))) (Proofterm.proof_combP (prf_of thm',
   34.42 +            map PBound (length prems - 1 downto 0))) (prems ~~ rs)));
   34.43      val r' = Logic.varify (Abs ("y", Type.varifyT T,
   34.44        list_abs (map dest_Free rs, list_comb (r,
   34.45          map Bound ((length rs - 1 downto 0) @ [length rs])))));
    35.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Mar 04 11:44:26 2005 +0100
    35.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Mar 04 15:07:34 2005 +0100
    35.3 @@ -78,7 +78,7 @@
    35.4      val branchT = if null branchTs then HOLogic.unitT
    35.5        else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
    35.6      val arities = get_arities descr' \ 0;
    35.7 -    val unneeded_vars = hd tyvars \\ Library.foldr add_typ_tfree_names (leafTs' @ branchTs, []);
    35.8 +    val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names [] (leafTs' @ branchTs);
    35.9      val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars);
   35.10      val recTs = get_rec_types descr' sorts;
   35.11      val newTs = Library.take (length (hd descr), recTs);
   35.12 @@ -134,7 +134,7 @@
   35.13        in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
   35.14        end;
   35.15  
   35.16 -    val mk_lim = Library.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
   35.17 +    val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
   35.18  
   35.19      (************** generate introduction rules for representing set **********)
   35.20  
   35.21 @@ -153,14 +153,14 @@
   35.22                in (j + 1, list_all (map (pair "x") Ts,
   35.23                    HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
   35.24                      Const (List.nth (rep_set_names, k), UnivT)))) :: prems,
   35.25 -                mk_lim (Ts, free_t) :: ts)
   35.26 +                mk_lim free_t Ts :: ts)
   35.27                end
   35.28            | _ =>
   35.29                let val T = typ_of_dtyp descr' sorts dt
   35.30                in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
   35.31                end);
   35.32  
   35.33 -        val (_, prems, ts) = Library.foldr mk_prem (cargs, (1, [], []));
   35.34 +        val (_, prems, ts) = foldr mk_prem (1, [], []) cargs;
   35.35          val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
   35.36            (mk_univ_inj ts n i, Const (s, UnivT)))
   35.37        in Logic.list_implies (prems, concl)
   35.38 @@ -210,13 +210,13 @@
   35.39            let val T = typ_of_dtyp descr' sorts dt;
   35.40                val free_t = mk_Free "x" T j
   35.41            in (case (strip_dtyp dt, strip_type T) of
   35.42 -              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us,
   35.43 -                Const (List.nth (all_rep_names, m), U --> Univ_elT) $
   35.44 -                  app_bnds free_t (length Us)) :: r_args)
   35.45 +              ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim
   35.46 +                (Const (List.nth (all_rep_names, m), U --> Univ_elT) $
   35.47 +                   app_bnds free_t (length Us)) Us :: r_args)
   35.48              | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
   35.49            end;
   35.50  
   35.51 -        val (_, l_args, r_args) = Library.foldr constr_arg (cargs, (1, [], []));
   35.52 +        val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
   35.53          val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
   35.54          val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
   35.55          val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
   35.56 @@ -329,13 +329,13 @@
   35.57              val (Us, U) = strip_type T'
   35.58            in (case strip_dtyp dt of
   35.59                (_, DtRec j) => if j mem ks' then
   35.60 -                  (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds
   35.61 -                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))],
   35.62 +                  (i2 + 1, i2' + 1, ts @ [mk_lim (app_bnds
   35.63 +                     (mk_Free "y" (Us ---> Univ_elT) i2') (length Us)) Us],
   35.64                     Ts @ [Us ---> Univ_elT])
   35.65                  else
   35.66 -                  (i2 + 1, i2', ts @ [mk_lim (Us,
   35.67 -                     Const (List.nth (all_rep_names, j), U --> Univ_elT) $
   35.68 -                       app_bnds (mk_Free "x" T' i2) (length Us))], Ts)
   35.69 +                  (i2 + 1, i2', ts @ [mk_lim
   35.70 +                     (Const (List.nth (all_rep_names, j), U --> Univ_elT) $
   35.71 +                        app_bnds (mk_Free "x" T' i2) (length Us)) Us], Ts)
   35.72              | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
   35.73            end;
   35.74  
   35.75 @@ -380,8 +380,8 @@
   35.76  
   35.77        in (thy', char_thms' @ char_thms) end;
   35.78  
   35.79 -    val (thy5, iso_char_thms) = Library.foldr make_iso_defs
   35.80 -      (tl descr, (add_path flat_names big_name thy4, []));
   35.81 +    val (thy5, iso_char_thms) = foldr make_iso_defs
   35.82 +      (add_path flat_names big_name thy4, []) (tl descr);
   35.83  
   35.84      (* prove isomorphism properties *)
   35.85  
   35.86 @@ -469,8 +469,8 @@
   35.87        in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
   35.88        end;
   35.89  
   35.90 -    val (iso_inj_thms_unfolded, iso_elem_thms) = Library.foldr prove_iso_thms
   35.91 -      (tl descr, ([], map #3 newT_iso_axms));
   35.92 +    val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
   35.93 +      ([], map #3 newT_iso_axms) (tl descr);
   35.94      val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded;
   35.95  
   35.96      (* prove  x : dt_rep_set_i --> x : range dt_Rep_i *)
    36.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Mar 04 11:44:26 2005 +0100
    36.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Mar 04 15:07:34 2005 +0100
    36.3 @@ -49,12 +49,12 @@
    36.4    in (case concl_of thm of
    36.5        _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
    36.6          Const (s, _) =>
    36.7 -          let val cs = Library.foldr add_term_consts (prems_of thm, [])
    36.8 +          let val cs = foldr add_term_consts [] (prems_of thm)
    36.9            in (CodegenData.put
   36.10              {intros = Symtab.update ((s,
   36.11                 getOpt (Symtab.lookup (intros, s), []) @ [thm]), intros),
   36.12 -             graph = Library.foldr (uncurry (Graph.add_edge o pair s))
   36.13 -               (cs, Library.foldl add_node (graph, s :: cs)),
   36.14 +             graph = foldr (uncurry (Graph.add_edge o pair s))
   36.15 +               (Library.foldl add_node (graph, s :: cs)) cs,
   36.16               eqns = eqns} thy, thm)
   36.17            end
   36.18        | _ => (warn thm; p))
   36.19 @@ -190,7 +190,7 @@
   36.20  fun cprod ([], ys) = []
   36.21    | cprod (x :: xs, ys) = map (pair x) ys @ cprod (xs, ys);
   36.22  
   36.23 -fun cprods xss = Library.foldr (map op :: o cprod) (xss, [[]]);
   36.24 +fun cprods xss = foldr (map op :: o cprod) [[]] xss;
   36.25  
   36.26  datatype mode = Mode of (int list option list * int list) * mode option list;
   36.27  
   36.28 @@ -526,7 +526,7 @@
   36.29          NONE => gr
   36.30        | SOME (names, intrs) =>
   36.31            mk_ind_def thy gr dep names [] [] (prep_intrs intrs)))
   36.32 -            (gr, Library.foldr add_term_consts (ts, []))
   36.33 +            (gr, foldr add_term_consts [] ts)
   36.34  
   36.35  and mk_ind_def thy gr dep names modecs factorcs intrs =
   36.36    let val ids = map (mk_const_id (sign_of thy)) names
    37.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Mar 04 11:44:26 2005 +0100
    37.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 04 15:07:34 2005 +0100
    37.3 @@ -183,8 +183,8 @@
    37.4      fun varify (t, (i, ts)) =
    37.5        let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
    37.6        in (maxidx_of_term t', t'::ts) end;
    37.7 -    val (i, cs') = Library.foldr varify (cs, (~1, []));
    37.8 -    val (i', intr_ts') = Library.foldr varify (intr_ts, (i, []));
    37.9 +    val (i, cs') = foldr varify (~1, []) cs;
   37.10 +    val (i', intr_ts') = foldr varify (i, []) intr_ts;
   37.11      val rec_consts = Library.foldl add_term_consts_2 ([], cs');
   37.12      val intr_consts = Library.foldl add_term_consts_2 ([], intr_ts');
   37.13      fun unify (env, (cname, cT)) =
   37.14 @@ -271,12 +271,12 @@
   37.15  
   37.16  val remove_split = rewrite_rule [split_conv RS eq_reflection];
   37.17  
   37.18 -fun split_rule_vars vs rl = standard (remove_split (Library.foldr split_rule_var'
   37.19 -  (mg_prod_factors vs ([], Thm.prop_of rl), rl)));
   37.20 +fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
   37.21 +  rl (mg_prod_factors vs ([], Thm.prop_of rl))));
   37.22  
   37.23 -fun split_rule vs rl = standard (remove_split (Library.foldr split_rule_var'
   37.24 -  (List.mapPartial (fn (t as Var ((a, _), _)) =>
   37.25 -    Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)), rl)));
   37.26 +fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
   37.27 +  rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
   37.28 +      Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)))));
   37.29  
   37.30  
   37.31  (** process rules **)
   37.32 @@ -337,7 +337,7 @@
   37.33  
   37.34  fun mk_elims cs cTs params intr_ts intr_names =
   37.35    let
   37.36 -    val used = Library.foldr add_term_names (intr_ts, []);
   37.37 +    val used = foldr add_term_names [] intr_ts;
   37.38      val [aname, pname] = variantlist (["a", "P"], used);
   37.39      val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   37.40  
   37.41 @@ -353,7 +353,7 @@
   37.42          val a = Free (aname, T);
   37.43  
   37.44          fun mk_elim_prem (_, t, ts) =
   37.45 -          list_all_free (map dest_Free ((Library.foldr add_term_frees (t::ts, [])) \\ params),
   37.46 +          list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params),
   37.47              Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   37.48          val c_intrs = (List.filter (equal c o #1 o #1) intrs);
   37.49        in
   37.50 @@ -369,7 +369,7 @@
   37.51  
   37.52  fun mk_indrule cs cTs params intr_ts =
   37.53    let
   37.54 -    val used = Library.foldr add_term_names (intr_ts, []);
   37.55 +    val used = foldr add_term_names [] intr_ts;
   37.56  
   37.57      (* predicates for induction rule *)
   37.58  
   37.59 @@ -407,8 +407,8 @@
   37.60            HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   37.61  
   37.62        in list_all_free (frees,
   37.63 -           Logic.list_implies (map HOLogic.mk_Trueprop (Library.foldr mk_prem
   37.64 -             (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   37.65 +           Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   37.66 +             [] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))),
   37.67                 HOLogic.mk_Trueprop (valOf (pred_of u) $ t)))
   37.68        end;
   37.69  
   37.70 @@ -422,15 +422,15 @@
   37.71        let val T = HOLogic.dest_setT (fastype_of c);
   37.72            val ps = getOpt (assoc (factors, P), []);
   37.73            val Ts = prodT_factors [] ps T;
   37.74 -          val (frees, x') = Library.foldr (fn (T', (fs, s)) =>
   37.75 -            ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
   37.76 +          val (frees, x') = foldr (fn (T', (fs, s)) =>
   37.77 +            ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
   37.78            val tuple = mk_tuple [] ps T frees;
   37.79        in ((HOLogic.mk_binop "op -->"
   37.80          (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   37.81        end;
   37.82  
   37.83      val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   37.84 -        (fst (Library.foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   37.85 +        (fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds))))
   37.86  
   37.87    in (preds, ind_prems, mutual_ind_concl,
   37.88      map (apfst (fst o dest_Free)) factors)
   37.89 @@ -707,7 +707,7 @@
   37.90  
   37.91      val fp_name = if coind then gfp_name else lfp_name;
   37.92  
   37.93 -    val used = Library.foldr add_term_names (intr_ts, []);
   37.94 +    val used = foldr add_term_names [] intr_ts;
   37.95      val [sname, xname] = variantlist (["S", "x"], used);
   37.96  
   37.97      (* transform an introduction rule into a conjunction  *)
   37.98 @@ -723,11 +723,11 @@
   37.99          val Const ("op :", _) $ t $ u =
  37.100            HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
  37.101  
  37.102 -      in Library.foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
  37.103 -        (frees, foldr1 HOLogic.mk_conj
  37.104 +      in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
  37.105 +        (foldr1 HOLogic.mk_conj
  37.106            (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
  37.107              (map (subst o HOLogic.dest_Trueprop)
  37.108 -              (Logic.strip_imp_prems r))))
  37.109 +              (Logic.strip_imp_prems r)))) frees
  37.110        end
  37.111  
  37.112      (* make a disjunction of all introduction rules *)
    38.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Mar 04 11:44:26 2005 +0100
    38.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Mar 04 15:07:34 2005 +0100
    38.3 @@ -41,11 +41,11 @@
    38.4        | strip _ t = t;
    38.5    in strip (add_term_free_names (t, [])) t end;
    38.6  
    38.7 -fun relevant_vars prop = Library.foldr (fn
    38.8 +fun relevant_vars prop = foldr (fn
    38.9        (Var ((a, i), T), vs) => (case strip_type T of
   38.10          (_, Type (s, _)) => if s mem ["bool", "set"] then (a, T) :: vs else vs
   38.11        | _ => vs)
   38.12 -    | (_, vs) => vs) (term_vars prop, []);
   38.13 +    | (_, vs) => vs) [] (term_vars prop);
   38.14  
   38.15  fun params_of intr = map (fst o fst o dest_Var) (term_vars
   38.16    (snd (HOLogic.dest_mem (HOLogic.dest_Trueprop
   38.17 @@ -265,9 +265,9 @@
   38.18  
   38.19    in (Thm.name_of_thm rule, (vs,
   38.20      if rt = Extraction.nullt then rt else
   38.21 -      Library.foldr (uncurry lambda) (vs1, rt),
   38.22 -    Library.foldr forall_intr_prf (vs2, mk_prf rs prems (Proofterm.proof_combP
   38.23 -      (prf_of rrule, map PBound (length prems - 1 downto 0))))))
   38.24 +      foldr (uncurry lambda) rt vs1,
   38.25 +    foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
   38.26 +      (prf_of rrule, map PBound (length prems - 1 downto 0)))) vs2))
   38.27    end;
   38.28  
   38.29  fun add_rule (rss, r) =
    39.1 --- a/src/HOL/Tools/meson.ML	Fri Mar 04 11:44:26 2005 +0100
    39.2 +++ b/src/HOL/Tools/meson.ML	Fri Mar 04 15:07:34 2005 +0100
    39.3 @@ -188,7 +188,7 @@
    39.4       let fun name1 (th, (k,ths)) =
    39.5             (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
    39.6  
    39.7 -     in  fn ths => #2 (Library.foldr name1 (ths, (length ths, [])))  end;
    39.8 +     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    39.9  
   39.10   (*Find an all-negative support clause*)
   39.11   fun is_negative th = forall (not o #1) (literals (prop_of th));
   39.12 @@ -239,7 +239,7 @@
   39.13  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   39.14  local fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
   39.15  in
   39.16 -fun size_of_subgoals st = Library.foldr addconcl (prems_of st, 0)
   39.17 +fun size_of_subgoals st = foldr addconcl 0 (prems_of st)
   39.18  end;
   39.19  
   39.20  (*Negation Normal Form*)
   39.21 @@ -265,12 +265,12 @@
   39.22  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   39.23    The resulting clauses are HOL disjunctions.*)
   39.24  fun make_clauses ths =
   39.25 -    sort_clauses (map (generalize o nodups) (Library.foldr cnf (ths,[])));
   39.26 +    sort_clauses (map (generalize o nodups) (foldr cnf [] ths));
   39.27  
   39.28  (*Convert a list of clauses to (contrapositive) Horn clauses*)
   39.29  fun make_horns ths =
   39.30      name_thms "Horn#"
   39.31 -      (gen_distinct Drule.eq_thm_prop (Library.foldr (add_contras clause_rules) (ths,[])));
   39.32 +      (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
   39.33  
   39.34  (*Could simply use nprems_of, which would count remaining subgoals -- no
   39.35    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
    40.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Mar 04 11:44:26 2005 +0100
    40.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Mar 04 15:07:34 2005 +0100
    40.3 @@ -161,8 +161,8 @@
    40.4          else
    40.5            let
    40.6              val (_, _, eqns) = valOf (assoc (rec_eqns, fname));
    40.7 -            val (fnames', fnss', fns) = Library.foldr (trans eqns)
    40.8 -              (constrs, ((i, fname)::fnames, fnss, []))
    40.9 +            val (fnames', fnss', fns) = foldr (trans eqns)
   40.10 +              ((i, fname)::fnames, fnss, []) constrs
   40.11            in
   40.12              (fnames', (i, (fname, #1 (snd (hd eqns)), fns))::fnss')
   40.13            end
   40.14 @@ -192,10 +192,10 @@
   40.15  
   40.16  fun make_def sign fs (fname, ls, rec_name, tname) =
   40.17    let
   40.18 -    val rhs = Library.foldr (fn (T, t) => Abs ("", T, t)) 
   40.19 -	            ((map snd ls) @ [dummyT],
   40.20 -		     list_comb (Const (rec_name, dummyT),
   40.21 -				fs @ map Bound (0 ::(length ls downto 1))));
   40.22 +    val rhs = foldr (fn (T, t) => Abs ("", T, t)) 
   40.23 +	            (list_comb (Const (rec_name, dummyT),
   40.24 +				fs @ map Bound (0 ::(length ls downto 1))))
   40.25 +		    ((map snd ls) @ [dummyT]);
   40.26      val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
   40.27  		   Logic.mk_equals (Const (fname, dummyT), rhs))
   40.28    in Theory.inferT_axm sign defpair end;
   40.29 @@ -228,7 +228,7 @@
   40.30      val (eqns, atts) = split_list eqns_atts;
   40.31      val sg = Theory.sign_of thy;
   40.32      val dt_info = DatatypePackage.get_datatypes thy;
   40.33 -    val rec_eqns = Library.foldr (process_eqn sg) (map snd eqns, []);
   40.34 +    val rec_eqns = foldr (process_eqn sg) [] (map snd eqns);
   40.35      val tnames = distinct (map (#1 o snd) rec_eqns);
   40.36      val dts = find_dts dt_info tnames tnames;
   40.37      val main_fns = 
   40.38 @@ -241,9 +241,9 @@
   40.39  	    primrec_err ("datatypes " ^ commas_quote tnames ^ 
   40.40  			 "\nare not mutually recursive")
   40.41  	else snd (hd dts);
   40.42 -    val (fnames, fnss) = Library.foldr (process_fun sg descr rec_eqns)
   40.43 -	                       (main_fns, ([], []));
   40.44 -    val (fs, defs) = Library.foldr (get_fns fnss) (descr ~~ rec_names, ([], []));
   40.45 +    val (fnames, fnss) = foldr (process_fun sg descr rec_eqns)
   40.46 +	                       ([], []) main_fns;
   40.47 +    val (fs, defs) = foldr (get_fns fnss) ([], []) (descr ~~ rec_names);
   40.48      val defs' = map (make_def sg fs) defs;
   40.49      val names1 = map snd fnames;
   40.50      val names2 = map fst rec_eqns;
    41.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Mar 04 11:44:26 2005 +0100
    41.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Mar 04 15:07:34 2005 +0100
    41.3 @@ -91,7 +91,7 @@
    41.4      val (del, rest) = Library.partition (Library.equal c o fst) congs;
    41.5    in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
    41.6  
    41.7 -val add_congs = curry (Library.foldr (uncurry add_cong));
    41.8 +val add_congs = foldr (uncurry add_cong);
    41.9  
   41.10  end;
   41.11  
   41.12 @@ -272,7 +272,7 @@
   41.13  
   41.14  fun prepare_hints_old thy (ss, thms) =
   41.15    let val {simps, congs, wfs} = get_global_hints thy
   41.16 -  in (Classical.claset_of thy, ss addsimps simps, map #2 (add_congs thms congs), wfs) end;
   41.17 +  in (Classical.claset_of thy, ss addsimps simps, map #2 (add_congs congs thms), wfs) end;
   41.18  
   41.19  val add_recdef_old = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints_old false;
   41.20  
    42.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Mar 04 11:44:26 2005 +0100
    42.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri Mar 04 15:07:34 2005 +0100
    42.3 @@ -128,9 +128,9 @@
    42.4                     (List.concat (map (get_equations thy) cs));
    42.5                   val (gr3, fundef') = mk_fundef "" "fun "
    42.6                     (Graph.add_edge (dname, dep)
    42.7 -                     (Library.foldr (uncurry Graph.new_node) (map (fn k =>
    42.8 -                       (k, (SOME (EQN ("", dummyT, dname)), ""))) xs,
    42.9 -                         Graph.del_nodes xs gr2))) eqs''
   42.10 +                     (foldr (uncurry Graph.new_node) (Graph.del_nodes xs gr2)
   42.11 +                       (map (fn k =>
   42.12 +                         (k, (SOME (EQN ("", dummyT, dname)), ""))) xs))) eqs''
   42.13                 in put_code fundef' gr3 end
   42.14               else gr2)
   42.15           end
    43.1 --- a/src/HOL/Tools/record_package.ML	Fri Mar 04 11:44:26 2005 +0100
    43.2 +++ b/src/HOL/Tools/record_package.ML	Fri Mar 04 15:07:34 2005 +0100
    43.3 @@ -430,7 +430,7 @@
    43.4  
    43.5      val tsig = Sign.tsig_of sg;
    43.6      fun unify (t,env) = Type.unify tsig env t;
    43.7 -    val (subst,_) = Library.foldr unify (but_last args ~~ but_last Ts,(Vartab.empty,0));
    43.8 +    val (subst,_) = foldr unify (Vartab.empty,0) (but_last args ~~ but_last Ts);
    43.9      val flds' = map (apsnd ((Envir.norm_type subst) o varifyT)) flds;
   43.10    in (flds',(more,moreT)) end;
   43.11  
   43.12 @@ -504,7 +504,7 @@
   43.13  
   43.14  
   43.15  fun record_update_tr [t, u] =
   43.16 -      Library.foldr (op $) (rev (gen_fields_tr "_updates" "_update" updateN u), t)
   43.17 +      foldr (op $) t (rev (gen_fields_tr "_updates" "_update" updateN u))
   43.18    | record_update_tr ts = raise TERM ("record_update_tr", ts);
   43.19  
   43.20  fun update_name_tr (Free (x, T) :: ts) = Free (suffix updateN x, T) $$ ts
   43.21 @@ -584,7 +584,7 @@
   43.22                         val (args,rest) = splitargs (map fst flds') fargs;
   43.23                         val vartypes = map Type.varifyT types;
   43.24                         val argtypes = map to_type args;
   43.25 -                       val (subst,_) = Library.foldr unify (vartypes ~~ argtypes,(Vartab.empty,0));
   43.26 +                       val (subst,_) = foldr unify (Vartab.empty,0) (vartypes ~~ argtypes);
   43.27                         val alphas' = map ((Syntax.term_of_typ (! Syntax.show_sorts)) o 
   43.28                                            (Envir.norm_type subst) o Type.varifyT) 
   43.29                                           (but_last alphas);
   43.30 @@ -777,7 +777,7 @@
   43.31                                              ::map (apfst NameSpace.base) fs; 
   43.32                                  val (args',more) = split_last args; 
   43.33                                  val alphavars = map Type.varifyT (but_last alphas); 
   43.34 -                                val (subst,_)= Library.foldr unify (alphavars~~args',(Vartab.empty,0));
   43.35 +                                val (subst,_)= foldr unify (Vartab.empty,0) (alphavars~~args');
   43.36                                  val flds'' =map (apsnd ((Envir.norm_type subst)o(Type.varifyT)))
   43.37                                                  flds';
   43.38                                in flds''@field_lst more end
   43.39 @@ -1332,8 +1332,8 @@
   43.40      val ext_decl = (mk_extC (name,extT) fields_moreTs);
   43.41      (*     
   43.42      val ext_spec = Const ext_decl :== 
   43.43 -         (Library.foldr (uncurry lambda) 
   43.44 -            (vars@[more],(mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))))) 
   43.45 +         (foldr (uncurry lambda) 
   43.46 +            (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more]))) (vars@[more])) 
   43.47      *) 
   43.48      val ext_spec = list_comb (Const ext_decl,vars@[more]) :== 
   43.49           (mk_Abs name repT extT $ (foldr1 HOLogic.mk_prod (vars@[more])));
   43.50 @@ -1551,7 +1551,7 @@
   43.51   * of parent extensions, starting with the root of the record hierarchy 
   43.52  *) 
   43.53  fun mk_recordT extT parent_exts = 
   43.54 -    Library.foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) (parent_exts,extT);
   43.55 +    foldr (fn ((parent,Ts),T) => Type (parent, subst_last T Ts)) extT parent_exts;
   43.56  
   43.57  
   43.58  
   43.59 @@ -1605,7 +1605,7 @@
   43.60      val names = map fst fields;
   43.61      val extN = full bname;
   43.62      val types = map snd fields;
   43.63 -    val alphas_fields = Library.foldr add_typ_tfree_names (types,[]);
   43.64 +    val alphas_fields = foldr add_typ_tfree_names [] types;
   43.65      val alphas_ext = alphas inter alphas_fields; 
   43.66      val len = length fields;
   43.67      val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::wN::parent_variants);
   43.68 @@ -1663,7 +1663,7 @@
   43.69        let val (args',more) = chop_last args;
   43.70  	  fun mk_ext' (((name,T),args),more) = mk_ext (name,T) (args@[more]);
   43.71            fun build Ts = 
   43.72 -           Library.foldr mk_ext' (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')),more) 
   43.73 +           foldr mk_ext' more (prune n (extension_names ~~ Ts ~~ (chunks parent_chunks args')))
   43.74        in 
   43.75          if more = HOLogic.unit 
   43.76          then build (map recT (0 upto parent_len)) 
   43.77 @@ -1822,13 +1822,13 @@
   43.78        end; 
   43.79  
   43.80      val split_object_prop =
   43.81 -      let fun ALL vs t = Library.foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) (vs,t)
   43.82 +      let fun ALL vs t = foldr (fn ((v,T),t) => HOLogic.mk_all (v,T,t)) t vs
   43.83        in (ALL [dest_Free r0] (P $ r0)) === (ALL (map dest_Free all_vars_more) (P $ r_rec0))
   43.84        end;
   43.85  
   43.86  
   43.87      val split_ex_prop =
   43.88 -      let fun EX vs t = Library.foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) (vs,t)
   43.89 +      let fun EX vs t = foldr (fn ((v,T),t) => HOLogic.mk_exists (v,T,t)) t vs
   43.90        in (EX [dest_Free r0] (P $ r0)) === (EX (map dest_Free all_vars_more) (P $ r_rec0))
   43.91        end;
   43.92  
   43.93 @@ -2048,7 +2048,7 @@
   43.94      val init_env =
   43.95        (case parent of
   43.96          NONE => []
   43.97 -      | SOME (types, _) => Library.foldr Term.add_typ_tfrees (types, []));
   43.98 +      | SOME (types, _) => foldr Term.add_typ_tfrees [] types);
   43.99  
  43.100  
  43.101      (* fields *)
    44.1 --- a/src/HOL/Tools/refute.ML	Fri Mar 04 11:44:26 2005 +0100
    44.2 +++ b/src/HOL/Tools/refute.ML	Fri Mar 04 15:07:34 2005 +0100
    44.3 @@ -788,14 +788,14 @@
    44.4  								else
    44.5  									acc)
    44.6  							(* collect argument types *)
    44.7 -							val acc_args = Library.foldr collect_types (Ts, acc')
    44.8 +							val acc_args = foldr collect_types acc' Ts
    44.9  							(* collect constructor types *)
   44.10 -							val acc_constrs = Library.foldr collect_types (List.concat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs), acc_args)
   44.11 +							val acc_constrs = foldr collect_types acc_args (List.concat (map (fn (_, ds) => map (typ_of_dtyp descr typ_assoc) ds) constrs))
   44.12  						in
   44.13  							acc_constrs
   44.14  						end
   44.15  					| NONE =>  (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
   44.16 -						T ins (Library.foldr collect_types (Ts, acc)))
   44.17 +						T ins (foldr collect_types acc Ts))
   44.18  				| TFree _                => T ins acc
   44.19  				| TVar _                 => T ins acc)
   44.20  	in
   44.21 @@ -1297,8 +1297,8 @@
   44.22  	let
   44.23  		val Ts = binder_types (fastype_of t)
   44.24  	in
   44.25 -		Library.foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
   44.26 -			(Library.take (i, Ts), list_comb (t, map Bound (i-1 downto 0)))
   44.27 +		foldr (fn (T, t) => Abs ("<eta_expand>", T, t))
   44.28 +			(list_comb (t, map Bound (i-1 downto 0))) (Library.take (i, Ts))
   44.29  	end;
   44.30  
   44.31  (* ------------------------------------------------------------------------- *)
   44.32 @@ -2234,7 +2234,7 @@
   44.33  					val HOLogic_empty_set = Const ("{}", HOLogic_setT)
   44.34  					val HOLogic_insert    = Const ("insert", HOLogic_prodT --> HOLogic_setT --> HOLogic_setT)
   44.35  				in
   44.36 -					SOME (Library.foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) (pairs, HOLogic_empty_set))
   44.37 +					SOME (foldr (fn (pair, acc) => HOLogic_insert $ pair $ acc) HOLogic_empty_set pairs)
   44.38  				end
   44.39  			| Type ("prop", [])      =>
   44.40  				(case index_from_interpretation intr of
    45.1 --- a/src/HOL/Tools/specification_package.ML	Fri Mar 04 11:44:26 2005 +0100
    45.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Mar 04 15:07:34 2005 +0100
    45.3 @@ -141,7 +141,7 @@
    45.4  		val tsig = Sign.tsig_of (sign_of thy)
    45.5  		val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
    45.6  			       "Specificaton: Only free variables of sort 'type' allowed"
    45.7 -		val prop_closed = Library.foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop)
    45.8 +		val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
    45.9  	    in
   45.10  		(prop_closed,frees)
   45.11  	    end
   45.12 @@ -182,7 +182,7 @@
   45.13  	    in
   45.14  		HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
   45.15  	    end
   45.16 -	val ex_prop = Library.foldr mk_exist (proc_consts,prop)
   45.17 +	val ex_prop = foldr mk_exist prop proc_consts
   45.18  	val cnames = map (fst o dest_Const) proc_consts
   45.19  	fun post_process (arg as (thy,thm)) =
   45.20  	    let
    46.1 --- a/src/HOL/Tools/split_rule.ML	Fri Mar 04 11:44:26 2005 +0100
    46.2 +++ b/src/HOL/Tools/split_rule.ML	Fri Mar 04 15:07:34 2005 +0100
    46.3 @@ -103,14 +103,14 @@
    46.4  
    46.5  (*curries ALL function variables occurring in a rule's conclusion*)
    46.6  fun split_rule rl =
    46.7 -  Library.foldr split_rule_var' (Term.term_vars (concl_of rl), rl)
    46.8 +  foldr split_rule_var' rl (Term.term_vars (concl_of rl))
    46.9    |> remove_internal_split
   46.10    |> Drule.standard;
   46.11  
   46.12  fun complete_split_rule rl =
   46.13 -  fst (Library.foldr complete_split_rule_var
   46.14 -    (collect_vars ([], concl_of rl),
   46.15 -      (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))))
   46.16 +  fst (foldr complete_split_rule_var
   46.17 +    (rl, map (fst o fst o dest_Var) (Term.term_vars (#prop (Thm.rep_thm rl))))
   46.18 +    (collect_vars ([], concl_of rl)))
   46.19    |> remove_internal_split
   46.20    |> Drule.standard
   46.21    |> RuleCases.save rl;
    47.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Mar 04 11:44:26 2005 +0100
    47.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Mar 04 15:07:34 2005 +0100
    47.3 @@ -243,7 +243,7 @@
    47.4  
    47.5        val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
    47.6    in 
    47.7 -     Library.foldr add_nat_var (!nat_vars, body_e) 
    47.8 +     foldr add_nat_var body_e (!nat_vars) 
    47.9    end;
   47.10  
   47.11  
    48.1 --- a/src/HOL/hologic.ML	Fri Mar 04 11:44:26 2005 +0100
    48.2 +++ b/src/HOL/hologic.ML	Fri Mar 04 15:07:34 2005 +0100
    48.3 @@ -148,7 +148,7 @@
    48.4  
    48.5  fun all_const T = Const ("All", [T --> boolT] ---> boolT);
    48.6  fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
    48.7 -val list_all = Library.foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P));
    48.8 +fun list_all (vs,x) = foldr (fn ((x, T), P) => all_const T $ Abs (x, T, P)) x vs;
    48.9  
   48.10  fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);
   48.11  fun mk_exists (x, T, P) = exists_const T $ absfree (x, T, P);
   48.12 @@ -246,13 +246,13 @@
   48.13  
   48.14  local  (*currently unused*)
   48.15  
   48.16 -fun mk_tupleT Ts = Library.foldr mk_prodT (Ts, unitT);
   48.17 +fun mk_tupleT Ts = foldr mk_prodT unitT Ts;
   48.18  
   48.19  fun dest_tupleT (Type ("Product_Type.unit", [])) = []
   48.20    | dest_tupleT (Type ("*", [T, U])) = T :: dest_tupleT U
   48.21    | dest_tupleT T = raise TYPE ("dest_tupleT", [T], []);
   48.22  
   48.23 -fun mk_tuple ts = Library.foldr mk_prod (ts, unit);
   48.24 +fun mk_tuple ts = foldr mk_prod unit ts;
   48.25  
   48.26  fun dest_tuple (Const ("Product_Type.Unity", _)) = []
   48.27    | dest_tuple (Const ("Pair", _) $ t $ u) = t :: dest_tuple u
    49.1 --- a/src/HOLCF/domain/axioms.ML	Fri Mar 04 11:44:26 2005 +0100
    49.2 +++ b/src/HOLCF/domain/axioms.ML	Fri Mar 04 15:07:34 2005 +0100
    49.3 @@ -31,8 +31,8 @@
    49.4   val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %:x_name'));
    49.5  
    49.6    val when_def = ("when_def",%%:(dname^"_when") == 
    49.7 -     Library.foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
    49.8 -				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
    49.9 +     foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
   49.10 +				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
   49.11  
   49.12    fun con_def outer recu m n (_,args) = let
   49.13       fun idxs z x arg = (if is_lazy arg then fn t => %%:"up"`t else Id)
   49.14 @@ -43,7 +43,7 @@
   49.15       fun inj y 1 _ = y
   49.16       |   inj y _ 0 = %%:"sinl"`y
   49.17       |   inj y i j = %%:"sinr"`(inj y (i-1) (j-1));
   49.18 -  in Library.foldr /\# (args, outer (inj (parms args) m n)) end;
   49.19 +  in foldr /\# (outer (inj (parms args) m n)) args end;
   49.20  
   49.21    val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo 
   49.22  	Library.foldl (op `) (%%:(dname^"_when") , 
   49.23 @@ -57,15 +57,15 @@
   49.24    val dis_defs = let
   49.25  	fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
   49.26  		 mk_cRep_CFun(%%:(dname^"_when"),map 
   49.27 -			(fn (con',args) => (Library.foldr /\#
   49.28 -			   (args,if con'=con then %%:"TT" else %%:"FF"))) cons))
   49.29 +			(fn (con',args) => (foldr /\#
   49.30 +			   (if con'=con then %%:"TT" else %%:"FF") args)) cons))
   49.31  	in map ddef cons end;
   49.32  
   49.33    val sel_defs = let
   49.34  	fun sdef con n arg = (sel_of arg^"_def",%%:(sel_of arg) == 
   49.35  		 mk_cRep_CFun(%%:(dname^"_when"),map 
   49.36  			(fn (con',args) => if con'<>con then %%:"UU" else
   49.37 -			 Library.foldr /\# (args,Bound (length args - n))) cons));
   49.38 +			 foldr /\# (Bound (length args - n)) args) cons));
   49.39  	in List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end;
   49.40  
   49.41  
   49.42 @@ -114,11 +114,12 @@
   49.43  					 (allargs~~((allargs_cnt-1) downto 0)));
   49.44  	fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ 
   49.45  			   Bound (2*recs_cnt-i) $ Bound (recs_cnt-i);
   49.46 -	val capps = Library.foldr mk_conj (mapn rel_app 1 rec_args, mk_conj(
   49.47 +	val capps = foldr mk_conj (mk_conj(
   49.48  	   Bound(allargs_cnt+1)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns1),
   49.49 -	   Bound(allargs_cnt+0)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns2)));
   49.50 -        in Library.foldr mk_ex (allvns, Library.foldr mk_conj 
   49.51 -			      (map (defined o Bound) nonlazy_idxs,capps)) end;
   49.52 +	   Bound(allargs_cnt+0)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns2)))
   49.53 +           (mapn rel_app 1 rec_args);
   49.54 +        in foldr mk_ex (Library.foldr mk_conj 
   49.55 +			      (map (defined o Bound) nonlazy_idxs,capps)) allvns end;
   49.56        fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
   49.57  	 		proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
   49.58           		foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
    50.1 --- a/src/HOLCF/domain/library.ML	Fri Mar 04 11:44:26 2005 +0100
    50.2 +++ b/src/HOLCF/domain/library.ML	Fri Mar 04 15:07:34 2005 +0100
    50.3 @@ -18,8 +18,8 @@
    50.4  			     | itr (a::l) = f(a, itr l)
    50.5  in  itr l  end;
    50.6  fun foldr' f l = foldr'' f (l,Id);
    50.7 -fun map_cumulr f start xs = Library.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
    50.8 -						  (y::ys,res2)) (xs,([],start));
    50.9 +fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
   50.10 +						  (y::ys,res2)) ([],start) xs;
   50.11  
   50.12  
   50.13  fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
    51.1 --- a/src/HOLCF/domain/syntax.ML	Fri Mar 04 11:44:26 2005 +0100
    51.2 +++ b/src/HOLCF/domain/syntax.ML	Fri Mar 04 15:07:34 2005 +0100
    51.3 @@ -22,15 +22,14 @@
    51.4  			    else foldr' mk_sprodT (map opt_lazy args);
    51.5    fun freetvar s = let val tvar = mk_TFree s in
    51.6  		   if tvar mem typevars then freetvar ("t"^s) else tvar end;
    51.7 -  fun when_type (_   ,_,args) = Library.foldr (op ->>) (map third args,freetvar "t");
    51.8 +  fun when_type (_   ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
    51.9  in
   51.10    val dtype  = Type(dname,typevars);
   51.11    val dtype2 = foldr' mk_ssumT (map prod cons');
   51.12    val dnam = Sign.base_name dname;
   51.13    val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
   51.14    val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
   51.15 -  val const_when = (dnam^"_when",Library.foldr (op ->>) ((map when_type cons'),
   51.16 -					        dtype ->> freetvar "t"), NoSyn);
   51.17 +  val const_when = (dnam^"_when",foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
   51.18    val const_copy = (dnam^"_copy", dtypeprod ->> dtype  ->> dtype , NoSyn);
   51.19  end;
   51.20  
   51.21 @@ -42,7 +41,7 @@
   51.22  							 else      c::esc cs
   51.23  	|   esc []      = []
   51.24  	in implode o esc o Symbol.explode end;
   51.25 -  fun con (name,s,args) = (name,Library.foldr (op ->>) (map third args,dtype),s);
   51.26 +  fun con (name,s,args) = (name,foldr (op ->>) dtype (map third args),s);
   51.27    fun dis (con ,s,_   ) = (dis_name_ con, dtype->>trT,
   51.28  			   Mixfix(escape ("is_" ^ con), [], Syntax.max_pri));
   51.29  			(* stricly speaking, these constants have one argument,
    52.1 --- a/src/Provers/blast.ML	Fri Mar 04 11:44:26 2005 +0100
    52.2 +++ b/src/Provers/blast.ML	Fri Mar 04 15:07:34 2005 +0100
    52.3 @@ -751,8 +751,8 @@
    52.4              end
    52.5        (*substitute throughout "stack frame"; extract affected formulae*)
    52.6        fun subFrame ((Gs,Hs), (changed, frames)) =
    52.7 -	    let val (changed', Gs') = Library.foldr subForm (Gs, (changed, []))
    52.8 -                val (changed'', Hs') = Library.foldr subForm (Hs, (changed', []))
    52.9 +	    let val (changed', Gs') = foldr subForm (changed, []) Gs
   52.10 +                val (changed'', Hs') = foldr subForm (changed', []) Hs
   52.11              in  (changed'', (Gs',Hs')::frames)  end
   52.12        (*substitute throughout literals; extract affected ones*)
   52.13        fun subLit (lit, (changed, nlits)) =
   52.14 @@ -760,8 +760,8 @@
   52.15  	    in  if nlit aconv lit then (changed, nlit::nlits)
   52.16  		                  else ((nlit,true)::changed, nlits)
   52.17              end
   52.18 -      val (changed, lits') = Library.foldr subLit (lits, ([], []))
   52.19 -      val (changed', pairs') = Library.foldr subFrame (pairs, (changed, []))
   52.20 +      val (changed, lits') = foldr subLit ([], []) lits
   52.21 +      val (changed', pairs') = foldr subFrame (changed, []) pairs
   52.22    in  if !trace then writeln ("Substituting " ^ traceTerm sign u ^
   52.23  			      " for " ^ traceTerm sign t ^ " in branch" )
   52.24        else ();
   52.25 @@ -974,7 +974,7 @@
   52.26  				    then lim - (1+log(length rules))
   52.27  				    else lim   (*discourage branching updates*)
   52.28  			 val vars  = vars_in_vars vars
   52.29 -			 val vars' = Library.foldr add_terms_vars (prems, vars)
   52.30 +			 val vars' = foldr add_terms_vars vars prems
   52.31  			 val choices' = (ntrl, nbrs, PRV) :: choices
   52.32  			 val tacs' = (tac(updated,false,true)) 
   52.33                                       :: tacs  (*no duplication; rotate*)
   52.34 @@ -1101,7 +1101,7 @@
   52.35  		    then
   52.36  		     let val updated = ntrl < !ntrail (*branch updated*)
   52.37  			 val vars  = vars_in_vars vars
   52.38 -			 val vars' = Library.foldr add_terms_vars (prems, vars)
   52.39 +			 val vars' = foldr add_terms_vars vars prems
   52.40  			    (*duplicate H if md permits*)
   52.41  			 val dup = md (*earlier had "andalso vars' <> vars":
   52.42                                    duplicate only if the subgoal has new vars*)
    53.1 --- a/src/Provers/classical.ML	Fri Mar 04 11:44:26 2005 +0100
    53.2 +++ b/src/Provers/classical.ML	Fri Mar 04 15:07:34 2005 +0100
    53.3 @@ -214,7 +214,7 @@
    53.4      let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
    53.5      in  assume_tac      ORELSE'
    53.6          contr_tac       ORELSE'
    53.7 -        biresolve_tac (Library.foldr addrl (rls,[]))
    53.8 +        biresolve_tac (foldr addrl [] rls)
    53.9      end;
   53.10  
   53.11  (*Duplication of hazardous rules, for complete provers*)
   53.12 @@ -286,7 +286,7 @@
   53.13  fun rep_cs (CS args) = args;
   53.14  
   53.15  local
   53.16 -  fun wrap l tac = Library.foldr (fn ((name,tacf),w) => tacf w) (l, tac);
   53.17 +  fun wrap l tac = foldr (fn ((name,tacf),w) => tacf w) tac l;
   53.18  in
   53.19    fun appSWrappers (CS{swrappers,...}) = wrap swrappers;
   53.20    fun appWrappers  (CS{uwrappers,...}) = wrap uwrappers;
   53.21 @@ -316,7 +316,7 @@
   53.22  fun tag_brls' _ _ [] = []
   53.23    | tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
   53.24  
   53.25 -fun insert_tagged_list kbrls netpr = Library.foldr Tactic.insert_tagged_brl (kbrls, netpr);
   53.26 +fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
   53.27  
   53.28  (*Insert into netpair that already has nI intr rules and nE elim rules.
   53.29    Count the intr rules double (to account for swapify).  Negate to give the
   53.30 @@ -324,7 +324,7 @@
   53.31  fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
   53.32  fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
   53.33  
   53.34 -fun delete_tagged_list brls netpr = Library.foldr Tactic.delete_tagged_brl (brls, netpr);
   53.35 +fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
   53.36  fun delete x = delete_tagged_list (joinrules x);
   53.37  fun delete' x = delete_tagged_list (joinrules' x);
   53.38  
    54.1 --- a/src/Provers/induct_method.ML	Fri Mar 04 11:44:26 2005 +0100
    54.2 +++ b/src/Provers/induct_method.ML	Fri Mar 04 15:07:34 2005 +0100
    54.3 @@ -268,8 +268,8 @@
    54.4    | rename _ thm = thm;
    54.5  
    54.6  fun find_inductT ctxt insts =
    54.7 -  Library.foldr multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
    54.8 -    |> map (InductAttrib.find_inductT ctxt o fastype_of), [[]])
    54.9 +  foldr multiply [[]] (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
   54.10 +    |> map (InductAttrib.find_inductT ctxt o fastype_of))
   54.11    |> map join_rules |> List.concat |> map (rename insts);
   54.12  
   54.13  fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact
    55.1 --- a/src/Provers/order.ML	Fri Mar 04 11:44:26 2005 +0100
    55.2 +++ b/src/Provers/order.ML	Fri Mar 04 15:07:34 2005 +0100
    55.3 @@ -437,7 +437,7 @@
    55.4  
    55.5     (* Compute, for each adjacency list, the list with reversed edges,
    55.6        and concatenate these lists. *)
    55.7 -   val flipped = Library.foldr (op @) ((map flip g),nil)
    55.8 +   val flipped = foldr (op @) nil (map flip g)
    55.9   
   55.10   in assemble g flipped end    
   55.11        
   55.12 @@ -475,9 +475,9 @@
   55.13        let
   55.14     val _ = visited := u :: !visited
   55.15     val descendents =
   55.16 -       Library.foldr (fn ((v,l),ds) => if been_visited v then ds
   55.17 +       foldr (fn ((v,l),ds) => if been_visited v then ds
   55.18              else v :: dfs_visit g v @ ds)
   55.19 -        ((adjacent (op aconv) g u) ,nil)
   55.20 +        nil (adjacent (op aconv) g u)
   55.21        in
   55.22     finish := u :: !finish;
   55.23     descendents
   55.24 @@ -525,9 +525,9 @@
   55.25        let
   55.26     val _ = visited := u :: !visited
   55.27     val descendents =
   55.28 -       Library.foldr (fn ((v,l),ds) => if been_visited v then ds
   55.29 +       foldr (fn ((v,l),ds) => if been_visited v then ds
   55.30              else v :: dfs_visit g v @ ds)
   55.31 -        ( ((adjacent (op =) g u)) ,nil)
   55.32 +        nil (adjacent (op =) g u)
   55.33     in  descendents end
   55.34   
   55.35   in u :: dfs_visit g u end;
    56.1 --- a/src/Provers/simp.ML	Fri Mar 04 11:44:26 2005 +0100
    56.2 +++ b/src/Provers/simp.ML	Fri Mar 04 15:07:34 2005 +0100
    56.3 @@ -155,7 +155,7 @@
    56.4  		     in case f of
    56.5  			    Const(c,T) => 
    56.6  				if c mem ccs
    56.7 -				then Library.foldr add_hvars (args,hvars)
    56.8 +				then foldr add_hvars hvars args
    56.9  				else add_term_vars(tm,hvars)
   56.10  			  | _ => add_term_vars(tm,hvars)
   56.11  		     end
   56.12 @@ -167,7 +167,7 @@
   56.13  		if at then vars else add_term_vars(tm,vars)
   56.14  	fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
   56.15  		in if length(tml)=length(al)
   56.16 -		   then Library.foldr itf (tml~~al,vars)
   56.17 +		   then foldr itf vars (tml~~al)
   56.18  		   else vars
   56.19  		end
   56.20  	fun add_vars (tm,vars) = case tm of
   56.21 @@ -188,12 +188,12 @@
   56.22      val lhs = rhs_of_eq 1 thm'
   56.23      val rhs = lhs_of_eq nops thm'
   56.24      val asms = tl(rev(tl(prems_of thm')))
   56.25 -    val hvars = Library.foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
   56.26 +    val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms)
   56.27      val hvars = add_new_asm_vars new_asms (rhs,hvars)
   56.28      fun it_asms (asm,hvars) =
   56.29  	if atomic asm then add_new_asm_vars new_asms (asm,hvars)
   56.30  	else add_term_frees(asm,hvars)
   56.31 -    val hvars = Library.foldr it_asms (asms,hvars)
   56.32 +    val hvars = foldr it_asms hvars asms
   56.33      val hvs = map (#1 o dest_Var) hvars
   56.34      val refl1_tac = refl_tac 1
   56.35      fun norm_step_tac st = st |>
   56.36 @@ -249,13 +249,13 @@
   56.37      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
   56.38       net);
   56.39  
   56.40 -val insert_thms = Library.foldr insert_thm_warn;
   56.41 +val insert_thms = foldr insert_thm_warn;
   56.42  
   56.43  fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
   56.44                splits,split_consts}, thm) =
   56.45  let val thms = mk_simps thm
   56.46  in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
   56.47 -      simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net),
   56.48 +      simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms,
   56.49        splits=splits,split_consts=split_consts}
   56.50  end;
   56.51  
   56.52 @@ -265,7 +265,7 @@
   56.53                     splits,split_consts}, thms) =
   56.54  let val congs' = thms @ congs;
   56.55  in SS{auto_tac=auto_tac, congs= congs',
   56.56 -      cong_net= insert_thms (map mk_trans thms,cong_net),
   56.57 +      cong_net= insert_thms cong_net (map mk_trans thms),
   56.58        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
   56.59        splits=splits,split_consts=split_consts}
   56.60  end;
   56.61 @@ -294,13 +294,13 @@
   56.62      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
   56.63       net);
   56.64  
   56.65 -val delete_thms = Library.foldr delete_thm_warn;
   56.66 +val delete_thms = foldr delete_thm_warn;
   56.67  
   56.68  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net,
   56.69                     splits,split_consts}, thms) =
   56.70  let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
   56.71  in SS{auto_tac=auto_tac, congs= congs',
   56.72 -      cong_net= delete_thms(map mk_trans thms,cong_net),
   56.73 +      cong_net= delete_thms cong_net (map mk_trans thms),
   56.74        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net,
   56.75        splits=splits,split_consts=split_consts}
   56.76  end;
   56.77 @@ -314,7 +314,7 @@
   56.78  			   ([],simps'))
   56.79      val (thms,simps') = find(simps,[])
   56.80  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
   56.81 -      simps = simps', simp_net = delete_thms(thms,simp_net),
   56.82 +      simps = simps', simp_net = delete_thms simp_net thms,
   56.83        splits=splits,split_consts=split_consts}
   56.84  end;
   56.85  
   56.86 @@ -460,7 +460,7 @@
   56.87  	val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
   56.88  	val new_rws = flat(map mk_rew_rules thms);
   56.89  	val rwrls = map mk_trans (flat(map mk_rew_rules thms));
   56.90 -	val anet' = Library.foldr lhs_insert_thm (rwrls,anet)
   56.91 +	val anet' = foldr lhs_insert_thm anet rwrls
   56.92      in  if !tracing andalso not(null new_rws)
   56.93  	then (writeln"Adding rewrites:";  prths new_rws;  ())
   56.94  	else ();
    57.1 --- a/src/Provers/trancl.ML	Fri Mar 04 11:44:26 2005 +0100
    57.2 +++ b/src/Provers/trancl.ML	Fri Mar 04 15:07:34 2005 +0100
    57.3 @@ -327,7 +327,7 @@
    57.4  
    57.5     (* Compute, for each adjacency list, the list with reversed edges,
    57.6        and concatenate these lists. *)
    57.7 -   val flipped = Library.foldr (op @) ((map flip g),nil)
    57.8 +   val flipped = foldr (op @) nil (map flip g)
    57.9   
   57.10   in assemble g flipped end    
   57.11   
   57.12 @@ -351,9 +351,9 @@
   57.13        let
   57.14     val _ = visited := u :: !visited
   57.15     val descendents =
   57.16 -       Library.foldr (fn ((v,l),ds) => if been_visited v then ds
   57.17 +       foldr (fn ((v,l),ds) => if been_visited v then ds
   57.18              else v :: dfs_visit g v @ ds)
   57.19 -        ( ((adjacent eq_comp g u)) ,nil)
   57.20 +        nil (adjacent eq_comp g u)
   57.21     in  descendents end
   57.22   
   57.23   in u :: dfs_visit g u end;
    58.1 --- a/src/Provers/typedsimp.ML	Fri Mar 04 11:44:26 2005 +0100
    58.2 +++ b/src/Provers/typedsimp.ML	Fri Mar 04 15:07:34 2005 +0100
    58.3 @@ -70,7 +70,7 @@
    58.4      handle THM _ => (simp_rls, rl :: other_rls);
    58.5  
    58.6  (*Given the list rls, return the pair (simp_rls, other_rls).*)
    58.7 -fun process_rules rls = Library.foldr add_rule (rls, ([],[]));
    58.8 +fun process_rules rls = foldr add_rule ([],[]) rls;
    58.9  
   58.10  (*Given list of rewrite rules, return list of both forms, reject others*)
   58.11  fun process_rewrites rls = 
    59.1 --- a/src/Pure/General/lazy_seq.ML	Fri Mar 04 11:44:26 2005 +0100
    59.2 +++ b/src/Pure/General/lazy_seq.ML	Fri Mar 04 15:07:34 2005 +0100
    59.3 @@ -397,8 +397,8 @@
    59.4  	make (fn () => copy (f x))
    59.5      end
    59.6  
    59.7 -fun EVERY fs = Library.foldr THEN (fs, succeed)
    59.8 -fun FIRST fs = Library.foldr ORELSE (fs, fail)
    59.9 +fun EVERY fs = foldr THEN succeed fs
   59.10 +fun FIRST fs = foldr ORELSE fail fs
   59.11  
   59.12  fun TRY f x =
   59.13      make (fn () =>
    60.1 --- a/src/Pure/General/name_space.ML	Fri Mar 04 11:44:26 2005 +0100
    60.2 +++ b/src/Pure/General/name_space.ML	Fri Mar 04 15:07:34 2005 +0100
    60.3 @@ -102,7 +102,7 @@
    60.4      error ("Attempt to declare hidden name " ^ quote name)
    60.5    else Library.foldl (fn (tb, xname) => change add xname (name, tb)) (tab, accesses name);
    60.6  
    60.7 -fun extend (NameSpace tab, names) = NameSpace (Library.foldr extend_aux (names, tab));
    60.8 +fun extend (NameSpace tab, names) = NameSpace (foldr extend_aux tab names);
    60.9  
   60.10  
   60.11  (* merge *)             (*1st preferred over 2nd*)
   60.12 @@ -126,7 +126,7 @@
   60.13      Library.foldl (fn (tb, xname) => change del xname (name, tb))
   60.14        (tab, if fully then accesses name else [base name])));
   60.15  
   60.16 -fun hide fully (NameSpace tab, names) = NameSpace (Library.foldr (hide_aux fully) (names, tab));
   60.17 +fun hide fully (NameSpace tab, names) = NameSpace (foldr (hide_aux fully) tab names);
   60.18  
   60.19  
   60.20  (* intern / extern names *)
    61.1 --- a/src/Pure/General/seq.ML	Fri Mar 04 11:44:26 2005 +0100
    61.2 +++ b/src/Pure/General/seq.ML	Fri Mar 04 15:07:34 2005 +0100
    61.3 @@ -97,7 +97,7 @@
    61.4    | SOME (x, xq') => x :: list_of xq');
    61.5  
    61.6  (*conversion from list to sequence*)
    61.7 -fun of_list xs = Library.foldr cons (xs, empty);
    61.8 +fun of_list xs = foldr cons empty xs;
    61.9  
   61.10  
   61.11  (*map the function f over the sequence, making a new sequence*)
   61.12 @@ -203,8 +203,8 @@
   61.13  fun op APPEND (f, g) x =
   61.14    append (f x, make (fn () => pull (g x)));
   61.15  
   61.16 -fun EVERY fs = Library.foldr THEN (fs, succeed);
   61.17 -fun FIRST fs = Library.foldr ORELSE (fs, fail);
   61.18 +fun EVERY fs = foldr THEN succeed fs;
   61.19 +fun FIRST fs = foldr ORELSE fail fs;
   61.20  
   61.21  fun TRY f = ORELSE (f, succeed);
   61.22  
    62.1 --- a/src/Pure/General/table.ML	Fri Mar 04 11:44:26 2005 +0100
    62.2 +++ b/src/Pure/General/table.ML	Fri Mar 04 15:07:34 2005 +0100
    62.3 @@ -287,7 +287,7 @@
    62.4  fun lookup_multi tab_key = getOpt (lookup tab_key,[]);
    62.5  fun update_multi ((key, x), tab) = update ((key, x :: lookup_multi (tab, key)), tab);
    62.6  
    62.7 -fun make_multi pairs = Library.foldr update_multi (pairs, empty);
    62.8 +fun make_multi pairs = foldr update_multi empty pairs;
    62.9  fun dest_multi tab = List.concat (map (fn (key, xs) => map (Library.pair key) xs) (dest tab));
   62.10  fun merge_multi eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists eq xs xs')) tabs;
   62.11  fun merge_multi' eq tabs = join (fn (xs, xs') => SOME (gen_merge_lists' eq xs xs')) tabs;
    63.1 --- a/src/Pure/IsaPlanner/isand.ML	Fri Mar 04 11:44:26 2005 +0100
    63.2 +++ b/src/Pure/IsaPlanner/isand.ML	Fri Mar 04 15:07:34 2005 +0100
    63.3 @@ -108,7 +108,7 @@
    63.4        fun allify_prem_var (vt as (n,ty),t)  = 
    63.5            (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    63.6  
    63.7 -      fun allify_prem Ts p = Library.foldr allify_prem_var (Ts, p)
    63.8 +      fun allify_prem Ts p = foldr allify_prem_var p Ts
    63.9  
   63.10        val cTs = map (ctermify o Free) Ts
   63.11        val cterm_asms = map (ctermify o allify_prem Ts) premts
   63.12 @@ -167,7 +167,7 @@
   63.13      in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   63.14  
   63.15  fun allify_for_sg_term ctermify vs t =
   63.16 -    let val t_alls = Library.foldr allify_term (vs,t);
   63.17 +    let val t_alls = foldr allify_term t vs;
   63.18          val ct_alls = ctermify t_alls; 
   63.19      in 
   63.20        (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
   63.21 @@ -256,7 +256,7 @@
   63.22                  |> Drule.forall_intr_list cfvs
   63.23      in Drule.compose_single (solth', i, gth) end;
   63.24  
   63.25 -val export_solutions = Library.foldr (uncurry export_solution);
   63.26 +fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
   63.27  
   63.28  
   63.29  (* fix parameters of a subgoal "i", as free variables, and create an
    64.1 --- a/src/Pure/IsaPlanner/rw_inst.ML	Fri Mar 04 11:44:26 2005 +0100
    64.2 +++ b/src/Pure/IsaPlanner/rw_inst.ML	Fri Mar 04 15:07:34 2005 +0100
    64.3 @@ -124,7 +124,7 @@
    64.4  fun mk_renamings tgt rule_inst = 
    64.5      let
    64.6        val rule_conds = Thm.prems_of rule_inst
    64.7 -      val names = Library.foldr Term.add_term_names (tgt :: rule_conds, []);
    64.8 +      val names = foldr Term.add_term_names [] (tgt :: rule_conds);
    64.9        val (conds_tyvs,cond_vs) = 
   64.10            Library.foldl (fn ((tyvs, vs), t) => 
   64.11                      (Library.union
   64.12 @@ -135,11 +135,11 @@
   64.13        val termvars = map Term.dest_Var (Term.term_vars tgt); 
   64.14        val vars_to_fix = Library.union (termvars, cond_vs);
   64.15        val (renamings, names2) = 
   64.16 -          Library.foldr (fn (((n,i),ty), (vs, names')) => 
   64.17 +          foldr (fn (((n,i),ty), (vs, names')) => 
   64.18                      let val n' = Term.variant names' n in
   64.19                        ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   64.20                      end)
   64.21 -                (vars_to_fix, ([], names));
   64.22 +                ([], names) vars_to_fix;
   64.23      in renamings end;
   64.24  
   64.25  (* make a new fresh typefree instantiation for the given tvar *)
   64.26 @@ -152,12 +152,12 @@
   64.27     already instantiated (in ignore_ixs) from the list of terms. *)
   64.28  fun mk_fixtvar_tyinsts ignore_ixs ts = 
   64.29      let val (tvars, tfreenames) = 
   64.30 -            Library.foldr (fn (t, (varixs, tfreenames)) => 
   64.31 +            foldr (fn (t, (varixs, tfreenames)) => 
   64.32                        (Term.add_term_tvars (t,varixs),
   64.33                         Term.add_term_tfree_names (t,tfreenames)))
   64.34 -                  (ts, ([],[]));
   64.35 +                  ([],[]) ts;
   64.36          val unfixed_tvars = List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
   64.37 -        val (fixtyinsts, _) = Library.foldr new_tfree (unfixed_tvars, ([], tfreenames))
   64.38 +        val (fixtyinsts, _) = foldr new_tfree ([], tfreenames) unfixed_tvars
   64.39      in (fixtyinsts, tfreenames) end;
   64.40  
   64.41  
   64.42 @@ -222,10 +222,10 @@
   64.43            Term.subst_vars (typinsts,[]) outerterm;
   64.44  
   64.45        (* type-instantiate the var instantiations *)
   64.46 -      val insts_tyinst = Library.foldr (fn ((ix,t),insts_tyinst) => 
   64.47 +      val insts_tyinst = foldr (fn ((ix,t),insts_tyinst) => 
   64.48                              (ix, Term.subst_vars (typinsts,[]) t)
   64.49                              :: insts_tyinst)
   64.50 -                        (unprepinsts,[]);
   64.51 +                        [] unprepinsts;
   64.52  
   64.53        (* cross-instantiate *)
   64.54        val insts_tyinst_inst = cross_inst insts_tyinst;
    65.1 --- a/src/Pure/Isar/context_rules.ML	Fri Mar 04 11:44:26 2005 +0100
    65.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Mar 04 15:07:34 2005 +0100
    65.3 @@ -203,7 +203,7 @@
    65.4  
    65.5  fun gen_wrap which ctxt =
    65.6    let val Rules {wrappers, ...} = LocalRules.get ctxt
    65.7 -  in fn tac => Library.foldr (fn ((w, _), t) => w t) (which wrappers, tac) end;
    65.8 +  in fn tac => foldr (fn ((w, _), t) => w t) tac (which wrappers) end;
    65.9  
   65.10  val Swrap = gen_wrap #1;
   65.11  val wrap = gen_wrap #2;
    66.1 --- a/src/Pure/Isar/locale.ML	Fri Mar 04 11:44:26 2005 +0100
    66.2 +++ b/src/Pure/Isar/locale.ML	Fri Mar 04 15:07:34 2005 +0100
    66.3 @@ -276,7 +276,7 @@
    66.4          val cert = Thm.cterm_of sign;
    66.5          val certT = Thm.ctyp_of sign;
    66.6          val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
    66.7 -        val tfrees = Library.foldr Term.add_term_tfree_names (prop :: hyps, []);
    66.8 +        val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
    66.9          val env' = List.filter (fn ((a, _), _) => a mem_string tfrees) env;
   66.10        in
   66.11          if null env' then th
   66.12 @@ -395,7 +395,7 @@
   66.13      val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
   66.14  
   66.15      fun inst_parms (i, ps) =
   66.16 -      Library.foldr Term.add_typ_tfrees (List.mapPartial snd ps, [])
   66.17 +      foldr Term.add_typ_tfrees [] (List.mapPartial snd ps)
   66.18        |> List.mapPartial (fn (a, S) =>
   66.19            let val T = Envir.norm_type unifier' (TVar ((a, i), S))
   66.20            in if T = TFree (a, S) then NONE else SOME ((a, S), T) end)
   66.21 @@ -1049,7 +1049,7 @@
   66.22            handle UnequalLengths => error "Number of parameters does not \
   66.23              \match number of arguments of chained fact";
   66.24      (* get their sorts *)
   66.25 -    val tfrees = Library.foldr Term.add_typ_tfrees (param_types, []);
   66.26 +    val tfrees = foldr Term.add_typ_tfrees [] param_types
   66.27      val Tenv' = map
   66.28            (fn ((a, i), T) => ((a, valOf (assoc_string (tfrees, a))), T))
   66.29            (Vartab.dest Tenv);
   66.30 @@ -1076,7 +1076,7 @@
   66.31  	    val cert = Thm.cterm_of sign;
   66.32  	    val certT = Thm.ctyp_of sign;
   66.33  	    val {hyps, prop, maxidx, ...} = Thm.rep_thm th;
   66.34 -	    val tfrees = Library.foldr Term.add_term_tfree_names (prop :: hyps, []);
   66.35 +	    val tfrees = foldr Term.add_term_tfree_names [] (prop :: hyps);
   66.36  	    val Tenv' = List.filter (fn ((a, _), _) => a mem_string tfrees) Tenv;
   66.37  	  in
   66.38  	    if null Tenv' then th
   66.39 @@ -1278,7 +1278,7 @@
   66.40  
   66.41  fun atomize_spec sign ts =
   66.42    let
   66.43 -    val t = Library.foldr1 Logic.mk_conjunction ts;
   66.44 +    val t = foldr1 Logic.mk_conjunction ts;
   66.45      val body = ObjectLogic.atomize_term sign t;
   66.46      val bodyT = Term.fastype_of body;
   66.47    in
   66.48 @@ -1308,7 +1308,7 @@
   66.49      val env = Term.add_term_free_names (body, []);
   66.50      val xs = List.filter (fn (x, _) => x mem_string env) parms;
   66.51      val Ts = map #2 xs;
   66.52 -    val extraTs = (Term.term_tfrees body \\ Library.foldr Term.add_typ_tfrees (Ts, []))
   66.53 +    val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
   66.54        |> Library.sort_wrt #1 |> map TFree;
   66.55      val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
   66.56  
    67.1 --- a/src/Pure/Isar/method.ML	Fri Mar 04 11:44:26 2005 +0100
    67.2 +++ b/src/Pure/Isar/method.ML	Fri Mar 04 15:07:34 2005 +0100
    67.3 @@ -309,7 +309,7 @@
    67.4  (* assumption *)
    67.5  
    67.6  fun asm_tac ths =
    67.7 -  Library.foldr (op APPEND') (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths, K no_tac);
    67.8 +  foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
    67.9  
   67.10  fun assm_tac ctxt =
   67.11    assume_tac APPEND'
    68.1 --- a/src/Pure/Isar/net_rules.ML	Fri Mar 04 11:44:26 2005 +0100
    68.2 +++ b/src/Pure/Isar/net_rules.ML	Fri Mar 04 15:07:34 2005 +0100
    68.3 @@ -51,7 +51,7 @@
    68.4  
    68.5  fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    68.6    let val rules = Library.gen_merge_lists' eq rules1 rules2
    68.7 -  in Library.foldr (uncurry add) (rules, init eq index) end;
    68.8 +  in foldr (uncurry add) (init eq index) rules end;
    68.9  
   68.10  fun delete rule (rs as Rules {eq, index, rules, next, net}) =
   68.11    if not (Library.gen_mem eq (rule, rules)) then rs
    69.1 --- a/src/Pure/Isar/proof.ML	Fri Mar 04 11:44:26 2005 +0100
    69.2 +++ b/src/Pure/Isar/proof.ML	Fri Mar 04 15:07:34 2005 +0100
    69.3 @@ -758,8 +758,8 @@
    69.4      val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
    69.5      val goal = Drule.mk_triv_goal cprop;
    69.6  
    69.7 -    val tvars = Library.foldr Term.add_term_tvars (props, []);
    69.8 -    val vars = Library.foldr Term.add_term_vars (props, []);
    69.9 +    val tvars = foldr Term.add_term_tvars [] props;
   69.10 +    val vars = foldr Term.add_term_vars [] props;
   69.11    in
   69.12      if null tvars then ()
   69.13      else raise STATE ("Goal statement contains illegal schematic type variable(s): " ^
    70.1 --- a/src/Pure/Isar/proof_context.ML	Fri Mar 04 11:44:26 2005 +0100
    70.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 04 15:07:34 2005 +0100
    70.3 @@ -697,7 +697,7 @@
    70.4  val ins_occs = foldl_term_types (fn t => foldl_atyps
    70.5    (fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab) | (tab, _) => tab));
    70.6  
    70.7 -fun ins_skolem def_ty = Library.foldr
    70.8 +fun ins_skolem def_ty = foldr
    70.9    (fn ((x, x'), types) =>
   70.10      (case def_ty x' of
   70.11        SOME T => Vartab.update (((x, ~1), T), types)
   70.12 @@ -716,7 +716,7 @@
   70.13    declare_syn (ctxt, t)
   70.14    |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
   70.15    |> map_defaults (fn (types, sorts, used, occ) =>
   70.16 -      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, used, occ));
   70.17 +      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) types fixes, sorts, used, occ));
   70.18  
   70.19  in
   70.20  
   70.21 @@ -773,7 +773,7 @@
   70.22  
   70.23  fun generalize inner outer ts =
   70.24    let
   70.25 -    val tfrees = generalize_tfrees inner outer (Library.foldr Term.add_term_tfree_names (ts, []));
   70.26 +    val tfrees = generalize_tfrees inner outer (foldr Term.add_term_tfree_names [] ts);
   70.27      fun gen (x, S) = if x mem_string tfrees then TVar ((x, 0), S) else TFree (x, S);
   70.28    in map (Term.map_term_types (Term.map_type_tfree gen)) ts end;
   70.29  
   70.30 @@ -1267,8 +1267,8 @@
   70.31        | replace [] ys = ys
   70.32        | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
   70.33    in
   70.34 -    if null (Library.foldr Term.add_typ_tvars (map snd fixes, [])) andalso
   70.35 -      null (Library.foldr Term.add_term_vars (List.concat (map snd assumes), [])) then
   70.36 +    if null (foldr Term.add_typ_tvars [] (map snd fixes)) andalso
   70.37 +      null (foldr Term.add_term_vars [] (List.concat (map snd assumes))) then
   70.38          {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds}
   70.39      else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
   70.40    end;
    71.1 --- a/src/Pure/Isar/rule_cases.ML	Fri Mar 04 11:44:26 2005 +0100
    71.2 +++ b/src/Pure/Isar/rule_cases.ML	Fri Mar 04 15:07:34 2005 +0100
    71.3 @@ -120,8 +120,8 @@
    71.4  
    71.5  fun make is_open split (sg, prop) names =
    71.6    let val nprems = Logic.count_prems (prop, 0) in
    71.7 -    Library.foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
    71.8 -      (Library.drop (length names - nprems, names), ([], length names)) |> #1
    71.9 +    foldr (fn (name, (cases, i)) => (prep_case is_open split sg prop name i :: cases, i - 1))
   71.10 +      ([], length names) (Library.drop (length names - nprems, names)) |> #1
   71.11    end;
   71.12  
   71.13  
    72.1 --- a/src/Pure/Proof/extraction.ML	Fri Mar 04 11:44:26 2005 +0100
    72.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 04 15:07:34 2005 +0100
    72.3 @@ -86,7 +86,7 @@
    72.4  
    72.5  fun merge_rules
    72.6    ({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
    72.7 -  Library.foldr add_rule (rs2 \\ rs1, {next = next, rs = rs1, net = net});
    72.8 +  foldr add_rule {next = next, rs = rs1, net = net} (rs2 \\ rs1);
    72.9  
   72.10  fun condrew sign rules procs =
   72.11    let
   72.12 @@ -147,7 +147,7 @@
   72.13    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   72.14    in Abst (a, SOME T, prf_abstract_over t prf) end;
   72.15  
   72.16 -val mkabs = Library.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
   72.17 +val mkabs = foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
   72.18  
   72.19  fun strip_abs 0 t = t
   72.20    | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
   72.21 @@ -156,11 +156,11 @@
   72.22  fun prf_subst_TVars tye =
   72.23    map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
   72.24  
   72.25 -fun relevant_vars types prop = Library.foldr (fn
   72.26 +fun relevant_vars types prop = foldr (fn
   72.27        (Var ((a, i), T), vs) => (case strip_type T of
   72.28          (_, Type (s, _)) => if s mem types then a :: vs else vs
   72.29        | _ => vs)
   72.30 -    | (_, vs) => vs) (vars_of prop, []);
   72.31 +    | (_, vs) => vs) [] (vars_of prop);
   72.32  
   72.33  fun tname_of (Type (s, _)) = s
   72.34    | tname_of _ = "";
   72.35 @@ -254,7 +254,7 @@
   72.36      defs, expand, prep} = ExtractionData.get thy;
   72.37    in
   72.38      ExtractionData.put
   72.39 -      {realizes_eqns = Library.foldr add_rule (map (prep_eq thy) eqns, realizes_eqns),
   72.40 +      {realizes_eqns = foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
   72.41         typeof_eqns = typeof_eqns, types = types, realizers = realizers,
   72.42         defs = defs, expand = expand, prep = prep} thy
   72.43    end
   72.44 @@ -272,7 +272,7 @@
   72.45    in
   72.46      ExtractionData.put
   72.47        {realizes_eqns = realizes_eqns, realizers = realizers,
   72.48 -       typeof_eqns = Library.foldr add_rule (eqns', typeof_eqns),
   72.49 +       typeof_eqns = foldr add_rule typeof_eqns eqns',
   72.50         types = types, defs = defs, expand = expand, prep = prep} thy
   72.51    end
   72.52  
   72.53 @@ -311,8 +311,8 @@
   72.54    in
   72.55      ExtractionData.put
   72.56        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
   72.57 -       realizers = Library.foldr Symtab.update_multi
   72.58 -         (map (prep_rlz thy) (rev rs), realizers),
   72.59 +       realizers = foldr Symtab.update_multi
   72.60 +         realizers (map (prep_rlz thy) (rev rs)),
   72.61         defs = defs, expand = expand, prep = prep} thy
   72.62    end
   72.63  
   72.64 @@ -344,7 +344,7 @@
   72.65          (procs @ [typeof_proc (Sign.defaultS sign) vs, rlz_proc]))
   72.66            (Const ("realizes", T --> propT --> propT) $
   72.67              (if T = nullT then t else list_comb (t, vars')) $ prop);
   72.68 -      val r = Library.foldr forall_intr (map (get_var_type r') vars, r');
   72.69 +      val r = foldr forall_intr r' (map (get_var_type r') vars);
   72.70        val prf = Reconstruct.reconstruct_proof sign r (rd s2);
   72.71      in (name, (vs, (t, prf))) end
   72.72    end;
   72.73 @@ -448,7 +448,7 @@
   72.74              end
   72.75            else (vs', tye)
   72.76  
   72.77 -      in Library.foldr add_args (Library.take (n, vars) ~~ Library.take (n, ts), ([], [])) end;
   72.78 +      in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
   72.79  
   72.80      fun find vs = Option.map snd o find_first (curry eq_set vs o fst);
   72.81      fun find' s = map snd o List.filter (equal s o fst)
   72.82 @@ -543,10 +543,11 @@
   72.83                      val (defs'', corr_prf) =
   72.84                        corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
   72.85                      val corr_prop = Reconstruct.prop_of corr_prf;
   72.86 -                    val corr_prf' = Library.foldr forall_intr_prf
   72.87 -                      (map (get_var_type corr_prop) (vfs_of prop), proof_combt
   72.88 +                    val corr_prf' = foldr forall_intr_prf
   72.89 +                      (proof_combt
   72.90                           (PThm ((corr_name name vs', []), corr_prf, corr_prop,
   72.91                               SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
   72.92 +		      (map (get_var_type corr_prop) (vfs_of prop))
   72.93                    in
   72.94                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
   72.95                       prf_subst_TVars tye' corr_prf')
   72.96 @@ -630,11 +631,11 @@
   72.97                      val args = filter_out (fn v => tname_of (body_type
   72.98                        (fastype_of v)) mem rtypes) (vfs_of prop);
   72.99                      val args' = List.filter (fn v => Logic.occs (v, nt)) args;
  72.100 -                    val t' = mkabs (args', nt);
  72.101 +                    val t' = mkabs nt args';
  72.102                      val T = fastype_of t';
  72.103                      val cname = extr_name s vs';
  72.104                      val c = Const (cname, T);
  72.105 -                    val u = mkabs (args, list_comb (c, args'));
  72.106 +                    val u = mkabs (list_comb (c, args')) args;
  72.107                      val eqn = Logic.mk_equals (c, t');
  72.108                      val rlz =
  72.109                        Const ("realizes", fastype_of nt --> propT --> propT);
  72.110 @@ -651,10 +652,11 @@
  72.111                             PAxm (cname ^ "_def", eqn,
  72.112                               SOME (map TVar (term_tvars eqn))))) %% corr_prf;
  72.113                      val corr_prop = Reconstruct.prop_of corr_prf';
  72.114 -                    val corr_prf'' = Library.foldr forall_intr_prf
  72.115 -                      (map (get_var_type corr_prop) (vfs_of prop), proof_combt
  72.116 +                    val corr_prf'' = foldr forall_intr_prf
  72.117 +                      (proof_combt
  72.118                          (PThm ((corr_name s vs', []), corr_prf', corr_prop,
  72.119 -                          SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop));
  72.120 +                          SOME (map TVar (term_tvars corr_prop))),  vfs_of corr_prop))
  72.121 +		      (map (get_var_type corr_prop) (vfs_of prop));
  72.122                    in
  72.123                      ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
  72.124                       subst_TVars tye' u)
    73.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 04 11:44:26 2005 +0100
    73.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Mar 04 15:07:34 2005 +0100
    73.3 @@ -228,7 +228,7 @@
    73.4                val tvars = term_tvars prop;
    73.5                val (_, rhs) = Logic.dest_equals prop;
    73.6                val rhs' = Library.foldl betapply (subst_TVars (map fst tvars ~~ Ts)
    73.7 -                (Library.foldr (fn p => Abs ("", dummyT, abstract_over p)) (vs, rhs)),
    73.8 +                (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
    73.9                  map valOf ts);
   73.10              in
   73.11                change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
    74.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Mar 04 11:44:26 2005 +0100
    74.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Mar 04 15:07:34 2005 +0100
    74.3 @@ -97,10 +97,10 @@
    74.4  
    74.5      val tab = Symtab.foldl (fn (tab, (key, ps)) =>
    74.6        let val prop = getOpt (assoc (thms', key), Bound 0)
    74.7 -      in fst (Library.foldr (fn ((prop', prf), x as (tab, i)) =>
    74.8 +      in fst (foldr (fn ((prop', prf), x as (tab, i)) =>
    74.9          if prop <> prop' then
   74.10            (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1)
   74.11 -        else x) (ps, (tab, 1)))
   74.12 +        else x) (tab, 1) ps)
   74.13        end) (Symtab.empty, thms);
   74.14  
   74.15      fun rename (Abst (s, T, prf)) = Abst (s, T, rename prf)
    75.1 --- a/src/Pure/Proof/proofchecker.ML	Fri Mar 04 11:44:26 2005 +0100
    75.2 +++ b/src/Pure/Proof/proofchecker.ML	Fri Mar 04 15:07:34 2005 +0100
    75.3 @@ -19,8 +19,8 @@
    75.4  (***** construct a theorem out of a proof term *****)
    75.5  
    75.6  fun lookup_thm thy =
    75.7 -  let val tab = Library.foldr Symtab.update
    75.8 -    (List.concat (map thms_of (thy :: Theory.ancestors_of thy)), Symtab.empty)
    75.9 +  let val tab = foldr Symtab.update Symtab.empty
   75.10 +    (List.concat (map thms_of (thy :: Theory.ancestors_of thy)))
   75.11    in
   75.12      (fn s => case Symtab.lookup (tab, s) of
   75.13         NONE => error ("Unknown theorem " ^ quote s)
    76.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Mar 04 11:44:26 2005 +0100
    76.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Mar 04 15:07:34 2005 +0100
    76.3 @@ -30,15 +30,15 @@
    76.4    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    76.5    in all T $ Abs (a, T, abstract_over (t, prop)) end;
    76.6  
    76.7 -fun forall_intr_vfs prop = Library.foldr forall_intr
    76.8 -  (vars_of prop @ sort (make_ord atless) (term_frees prop), prop);
    76.9 +fun forall_intr_vfs prop = foldr forall_intr prop
   76.10 +  (vars_of prop @ sort (make_ord atless) (term_frees prop));
   76.11  
   76.12  fun forall_intr_prf (t, prf) =
   76.13    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   76.14    in Abst (a, SOME T, prf_abstract_over t prf) end;
   76.15  
   76.16 -fun forall_intr_vfs_prf prop prf = Library.foldr forall_intr_prf
   76.17 -  (vars_of prop @ sort (make_ord atless) (term_frees prop), prf);
   76.18 +fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf prf
   76.19 +  (vars_of prop @ sort (make_ord atless) (term_frees prop));
   76.20  
   76.21  fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
   76.22    (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
    77.1 --- a/src/Pure/Syntax/printer.ML	Fri Mar 04 11:44:26 2005 +0100
    77.2 +++ b/src/Pure/Syntax/printer.ML	Fri Mar 04 15:07:34 2005 +0100
    77.3 @@ -246,7 +246,7 @@
    77.4    let
    77.5      val fmts = List.mapPartial xprod_to_fmt xprods;
    77.6      val tab = get_tab prtabs mode;
    77.7 -    val new_tab = Library.foldr Symtab.update_multi (rev fmts, tab);
    77.8 +    val new_tab = foldr Symtab.update_multi tab (rev fmts);
    77.9    in overwrite (prtabs, (mode, new_tab)) end;
   77.10  
   77.11  fun merge_prtabs prtabs1 prtabs2 =
    78.1 --- a/src/Pure/Syntax/syntax.ML	Fri Mar 04 11:44:26 2005 +0100
    78.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Mar 04 15:07:34 2005 +0100
    78.3 @@ -101,7 +101,7 @@
    78.4  (* print (ast) translations *)
    78.5  
    78.6  fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
    78.7 -fun extend_tr'tab tab trfuns = Library.foldr Symtab.update_multi (map mk_trfun trfuns, tab);
    78.8 +fun extend_tr'tab tab trfuns = foldr Symtab.update_multi tab (map mk_trfun trfuns);
    78.9  fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' eq_trfuns (tab1, tab2);
   78.10  
   78.11  
   78.12 @@ -154,7 +154,7 @@
   78.13  (* empty, extend, merge ruletabs *)
   78.14  
   78.15  fun extend_ruletab tab rules =
   78.16 -  Library.foldr Symtab.update_multi (map (fn r => (Ast.head_of_rule r, r)) rules, tab);
   78.17 +  foldr Symtab.update_multi tab (map (fn r => (Ast.head_of_rule r, r)) rules);
   78.18  
   78.19  fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
   78.20  
    79.1 --- a/src/Pure/codegen.ML	Fri Mar 04 11:44:26 2005 +0100
    79.2 +++ b/src/Pure/codegen.ML	Fri Mar 04 15:07:34 2005 +0100
    79.3 @@ -225,8 +225,8 @@
    79.4  fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
    79.5  
    79.6  val code_attr =
    79.7 -  Attrib.syntax (Scan.depend (fn thy => Library.foldr op || (map mk_parser
    79.8 -    (#attrs (CodegenData.get thy)), Scan.fail) >> pair thy));
    79.9 +  Attrib.syntax (Scan.depend (fn thy => foldr op || Scan.fail (map mk_parser
   79.10 +    (#attrs (CodegenData.get thy))) >> pair thy));
   79.11  
   79.12  
   79.13  (**** preprocessors ****)
   79.14 @@ -344,8 +344,8 @@
   79.15  
   79.16  fun rename_terms ts =
   79.17    let
   79.18 -    val names = Library.foldr add_term_names
   79.19 -      (ts, map (fst o fst) (Drule.vars_of_terms ts));
   79.20 +    val names = foldr add_term_names
   79.21 +      (map (fst o fst) (Drule.vars_of_terms ts)) ts;
   79.22      val reserved = names inter ThmDatabase.ml_reserved;
   79.23      val (illegal, alt_names) = split_list (List.mapPartial (fn s =>
   79.24        let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
   79.25 @@ -443,8 +443,8 @@
   79.26      val (Ts, _) = strip_type (fastype_of t);
   79.27      val j = i - length ts
   79.28    in
   79.29 -    Library.foldr (fn (T, t) => Abs ("x", T, t))
   79.30 -      (Library.take (j, Ts), list_comb (t, ts @ map Bound (j-1 downto 0)))
   79.31 +    foldr (fn (T, t) => Abs ("x", T, t))
   79.32 +      (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
   79.33    end;
   79.34  
   79.35  fun mk_app _ p [] = p
    80.1 --- a/src/Pure/display.ML	Fri Mar 04 11:44:26 2005 +0100
    80.2 +++ b/src/Pure/display.ML	Fri Mar 04 15:07:34 2005 +0100
    80.3 @@ -282,7 +282,7 @@
    80.4    | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
    80.5    | add_vars (_, env) = env;
    80.6  
    80.7 -fun add_varsT (Type (_, Ts), env) = Library.foldr add_varsT (Ts, env)
    80.8 +fun add_varsT (Type (_, Ts), env) = foldr add_varsT env Ts
    80.9    | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
   80.10    | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
   80.11  
    81.1 --- a/src/Pure/drule.ML	Fri Mar 04 11:44:26 2005 +0100
    81.2 +++ b/src/Pure/drule.ML	Fri Mar 04 15:07:34 2005 +0100
    81.3 @@ -343,10 +343,10 @@
    81.4    in Library.foldl elim (thm, Term.variantlist (map #1 vs, []) ~~ map #2 vs) end;
    81.5  
    81.6  (*Specialization over a list of cterms*)
    81.7 -fun forall_elim_list cts th = Library.foldr (uncurry forall_elim) (rev cts, th);
    81.8 +fun forall_elim_list cts th = foldr (uncurry forall_elim) th (rev cts);
    81.9  
   81.10  (* maps A1,...,An |- B   to   [| A1;...;An |] ==> B  *)
   81.11 -fun implies_intr_list cAs th = Library.foldr (uncurry implies_intr) (cAs,th);
   81.12 +fun implies_intr_list cAs th = foldr (uncurry implies_intr) th cAs;
   81.13  
   81.14  (* maps [| A1;...;An |] ==> B and [A1,...,An]   to   B *)
   81.15  fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
   81.16 @@ -364,12 +364,12 @@
   81.17  fun zero_var_indexes th =
   81.18      let val {prop,sign,tpairs,...} = rep_thm th;
   81.19          val (tpair_l, tpair_r) = Library.split_list tpairs;
   81.20 -        val vars = Library.foldr add_term_vars 
   81.21 -                         (tpair_r, Library.foldr add_term_vars (tpair_l, (term_vars prop)));
   81.22 +        val vars = foldr add_term_vars 
   81.23 +                         (foldr add_term_vars (term_vars prop) tpair_l) tpair_r;
   81.24          val bs = Library.foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars)
   81.25          val inrs = 
   81.26 -            Library.foldr add_term_tvars 
   81.27 -                  (tpair_r, Library.foldr add_term_tvars (tpair_l, (term_tvars prop)));
   81.28 +            foldr add_term_tvars 
   81.29 +                  (foldr add_term_tvars (term_tvars prop) tpair_l) tpair_r;
   81.30          val nms' = rev(Library.foldl add_new_id ([], map (#1 o #1) inrs));
   81.31          val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs)))
   81.32                       (inrs, nms')
   81.33 @@ -423,13 +423,13 @@
   81.34   let val fth = freezeT th
   81.35       val {prop, tpairs, sign, ...} = rep_thm fth
   81.36   in
   81.37 -   case Library.foldr add_term_vars (prop :: Thm.terms_of_tpairs tpairs, []) of
   81.38 +   case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   81.39         [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
   81.40       | vars =>
   81.41           let fun newName (Var(ix,_), pairs) =
   81.42                     let val v = gensym (string_of_indexname ix)
   81.43                     in  ((ix,v)::pairs)  end;
   81.44 -             val alist = Library.foldr newName (vars,[])
   81.45 +             val alist = foldr newName [] vars
   81.46               fun mk_inst (Var(v,T)) =
   81.47                   (cterm_of sign (Var(v,T)),
   81.48                    cterm_of sign (Free(valOf (assoc(alist,v)), T)))
   81.49 @@ -446,14 +446,14 @@
   81.50   let val fth = freezeT th
   81.51       val {prop, tpairs, sign, ...} = rep_thm fth
   81.52   in
   81.53 -   case Library.foldr add_term_vars (prop :: Thm.terms_of_tpairs tpairs, []) of
   81.54 +   case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   81.55         [] => (fth, fn x => x)
   81.56       | vars =>
   81.57           let fun newName (Var(ix,_), (pairs,used)) =
   81.58                     let val v = variant used (string_of_indexname ix)
   81.59                     in  ((ix,v)::pairs, v::used)  end;
   81.60 -             val (alist, _) = Library.foldr newName (vars, ([], Library.foldr add_term_names
   81.61 -               (prop :: Thm.terms_of_tpairs tpairs, [])))
   81.62 +             val (alist, _) = foldr newName ([], Library.foldr add_term_names
   81.63 +               (prop :: Thm.terms_of_tpairs tpairs, [])) vars
   81.64               fun mk_inst (Var(v,T)) =
   81.65                   (cterm_of sign (Var(v,T)),
   81.66                    cterm_of sign (Free(valOf (assoc(alist,v)), T)))
   81.67 @@ -641,9 +641,9 @@
   81.68  fun abs_def thm =
   81.69    let
   81.70      val (_, cvs) = strip_comb (fst (dest_equals (cprop_of thm)));
   81.71 -    val thm' = Library.foldr (fn (ct, thm) => Thm.abstract_rule
   81.72 +    val thm' = foldr (fn (ct, thm) => Thm.abstract_rule
   81.73        (case term_of ct of Var ((a, _), _) => a | Free (a, _) => a | _ => "x")
   81.74 -        ct thm) (cvs, thm)
   81.75 +        ct thm) thm cvs
   81.76    in transitive
   81.77      (symmetric (eta_conversion (fst (dest_equals (cprop_of thm'))))) thm'
   81.78    end;
   81.79 @@ -835,7 +835,7 @@
   81.80      in  (sign', tye', maxi')  end;
   81.81  in
   81.82  fun cterm_instantiate ctpairs0 th =
   81.83 -  let val (sign,tye,_) = Library.foldr add_types (ctpairs0, (Thm.sign_of_thm th, Vartab.empty, 0))
   81.84 +  let val (sign,tye,_) = foldr add_types (Thm.sign_of_thm th, Vartab.empty, 0) ctpairs0
   81.85        fun instT(ct,cu) = 
   81.86          let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
   81.87          in (inst ct, inst cu) end
   81.88 @@ -862,7 +862,7 @@
   81.89    handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
   81.90  
   81.91  (*Calling equal_abs_elim with multiple terms*)
   81.92 -fun equal_abs_elim_list cts th = Library.foldr (uncurry equal_abs_elim) (rev cts, th);
   81.93 +fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) th (rev cts);
   81.94  
   81.95  
   81.96  (*** Goal (PROP A) <==> PROP A ***)
   81.97 @@ -991,7 +991,7 @@
   81.98  
   81.99  fun tfrees_of thm =
  81.100    let val {hyps, prop, ...} = Thm.rep_thm thm
  81.101 -  in Library.foldr Term.add_term_tfree_names (prop :: hyps, []) end;
  81.102 +  in foldr Term.add_term_tfree_names [] (prop :: hyps) end;
  81.103  
  81.104  fun tvars_intr_list tfrees thm =
  81.105    Thm.varifyT' (tfrees_of thm \\ tfrees) thm;
    82.1 --- a/src/Pure/goals.ML	Fri Mar 04 11:44:26 2005 +0100
    82.2 +++ b/src/Pure/goals.ML	Fri Mar 04 15:07:34 2005 +0100
    82.3 @@ -307,8 +307,8 @@
    82.4      let val cur_sc = get_scope_sg sg;
    82.5          val rule_lists = map (#rules o snd) cur_sc;
    82.6          val def_lists = map (#defs o snd) cur_sc;
    82.7 -        val rules = map snd (Library.foldr (op union) (rule_lists, []));
    82.8 -        val defs = map snd (Library.foldr (op union) (def_lists, []));
    82.9 +        val rules = map snd (foldr (op union) [] rule_lists);
   82.10 +        val defs = map snd (foldr (op union) [] def_lists);
   82.11          val defnrules = rules @ defs;
   82.12      in
   82.13          hyps subset defnrules
    83.1 --- a/src/Pure/meta_simplifier.ML	Fri Mar 04 11:44:26 2005 +0100
    83.2 +++ b/src/Pure/meta_simplifier.ML	Fri Mar 04 15:07:34 2005 +0100
    83.3 @@ -1059,9 +1059,9 @@
    83.4                  find_index_eq p tprems) (#hyps (rep_thm eqn)));
    83.5                val (rrs', asm') = rules_of_prem ss prem'
    83.6              in mut_impc prems concl rrss asms (prem' :: prems')
    83.7 -              (rrs' :: rrss') (asm' :: asms') (SOME (Library.foldr (disch true)
    83.8 -                (Library.take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies
    83.9 -                  (Library.drop (i, prems), concl))))) :: eqns) ss (length prems') ~1
   83.10 +              (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)
   83.11 +                (Drule.imp_cong' eqn (reflexive (Drule.list_implies
   83.12 +                  (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns) ss (length prems') ~1
   83.13              end
   83.14  
   83.15       (*legacy code - only for backwards compatibility*)
    84.1 --- a/src/Pure/net.ML	Fri Mar 04 11:44:26 2005 +0100
    84.2 +++ b/src/Pure/net.ML	Fri Mar 04 15:07:34 2005 +0100
    84.3 @@ -165,9 +165,9 @@
    84.4  (*Skipping a term in a net.  Recursively skip 2 levels if a combination*)
    84.5  fun net_skip (Leaf _, nets) = nets
    84.6    | net_skip (Net{comb,var,alist}, nets) =
    84.7 -    Library.foldr net_skip
    84.8 -          (net_skip (comb,[]),
    84.9 -           Library.foldr (fn ((_,net), nets) => net::nets) (alist, var::nets));
   84.10 +    foldr net_skip
   84.11 +          (foldr (fn ((_,net), nets) => net::nets) (var::nets) alist)
   84.12 +          (net_skip (comb,[]))
   84.13  
   84.14  (** Matching and Unification**)
   84.15  
   84.16 @@ -185,7 +185,7 @@
   84.17    let fun rands _ (Leaf _, nets) = nets
   84.18          | rands t (Net{comb,alist,...}, nets) =
   84.19              case t of
   84.20 -                f$t => Library.foldr (matching unif t) (rands f (comb,[]), nets)
   84.21 +                f$t => foldr (matching unif t) nets (rands f (comb,[]))
   84.22                | Const(c,_) => look1 (alist, c) nets
   84.23                | Free(c,_)  => look1 (alist, c) nets
   84.24                | Bound i    => look1 (alist, string_of_bound i) nets
    85.1 --- a/src/Pure/pattern.ML	Fri Mar 04 11:44:26 2005 +0100
    85.2 +++ b/src/Pure/pattern.ML	Fri Mar 04 15:07:34 2005 +0100
    85.3 @@ -476,7 +476,7 @@
    85.4      val skel0 = Bound 0;
    85.5  
    85.6      val rhs_names =
    85.7 -      Library.foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) (rules, []);
    85.8 +      foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) [] rules;
    85.9  
   85.10      fun variant_absfree (x, T, t) =
   85.11        let
    86.1 --- a/src/Pure/proofterm.ML	Fri Mar 04 11:44:26 2005 +0100
    86.2 +++ b/src/Pure/proofterm.ML	Fri Mar 04 15:07:34 2005 +0100
    86.3 @@ -217,7 +217,7 @@
    86.4        (PThm (_, prf', _, _), _) => prf'
    86.5      | _ => prf);
    86.6  
    86.7 -val mk_Abst = Library.foldr (fn ((s, T:typ), prf) => Abst (s, NONE, prf));
    86.8 +val mk_Abst = foldr (fn ((s, T:typ), prf) => Abst (s, NONE, prf));
    86.9  fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
   86.10  
   86.11  fun apsome' f NONE = raise SAME
   86.12 @@ -254,8 +254,8 @@
   86.13    | fold_proof_terms f g (a, prf % NONE) = fold_proof_terms f g (a, prf)
   86.14    | fold_proof_terms f g (a, prf1 %% prf2) = fold_proof_terms f g
   86.15        (fold_proof_terms f g (a, prf1), prf2)
   86.16 -  | fold_proof_terms _ g (a, PThm (_, _, _, SOME Ts)) = Library.foldr g (Ts, a)
   86.17 -  | fold_proof_terms _ g (a, PAxm (_, prop, SOME Ts)) = Library.foldr g (Ts, a)
   86.18 +  | fold_proof_terms _ g (a, PThm (_, _, _, SOME Ts)) = foldr g a Ts
   86.19 +  | fold_proof_terms _ g (a, PAxm (_, prop, SOME Ts)) = foldr g a Ts
   86.20    | fold_proof_terms _ _ (a, _) = a;
   86.21  
   86.22  val add_prf_names = fold_proof_terms add_term_names ((uncurry K) o swap);
   86.23 @@ -557,7 +557,7 @@
   86.24    let
   86.25      val used = it_term_types add_typ_tfree_names (t, [])
   86.26      and tvars = map #1 (it_term_types add_typ_tvars (t, []));
   86.27 -    val (alist, _) = Library.foldr new_name (tvars, ([], used));
   86.28 +    val (alist, _) = foldr new_name ([], used) tvars;
   86.29    in
   86.30      (case alist of
   86.31        [] => prf (*nothing to do!*)
   86.32 @@ -579,9 +579,9 @@
   86.33      val j = length Bs;
   86.34    in
   86.35      mk_AbsP (j+1, proof_combP (prf, map PBound
   86.36 -      (j downto 1) @ [mk_Abst (params, mk_AbsP (i,
   86.37 +      (j downto 1) @ [mk_Abst (mk_AbsP (i,
   86.38          proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
   86.39 -          map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
   86.40 +          map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m)))))) params]))
   86.41    end;
   86.42  
   86.43  
   86.44 @@ -637,7 +637,7 @@
   86.45        | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = 
   86.46  	    Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
   86.47        | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
   86.48 -            map (fn k => (#3 (Library.foldr mk_app (bs, (i-1, j-1, PBound k)))))
   86.49 +            map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
   86.50                (i + k - 1 downto i));
   86.51    in
   86.52      mk_AbsP (k, lift [] [] 0 0 Bi)
   86.53 @@ -1127,7 +1127,7 @@
   86.54        map SOME (sort (make_ord atless) (term_frees prop));
   86.55      val opt_prf = if ! proofs = 2 then
   86.56          #4 (shrink [] 0 (rewrite_prf fst (ProofData.get_sg sign)
   86.57 -          (Library.foldr (uncurry implies_intr_proof) (hyps, prf))))
   86.58 +          (foldr (uncurry implies_intr_proof) prf hyps)))
   86.59        else MinProof (mk_min_proof ([], prf));
   86.60      val head = (case strip_combt (fst (strip_combP prf)) of
   86.61          (PThm ((old_name, _), prf', prop', NONE), args') =>
    87.1 --- a/src/Pure/search.ML	Fri Mar 04 11:44:26 2005 +0100
    87.2 +++ b/src/Pure/search.ML	Fri Mar 04 15:07:34 2005 +0100
    87.3 @@ -215,8 +215,8 @@
    87.4        fun pairsize th = (sizef th, th);
    87.5        fun bfs (news,nprf_heap) =
    87.6  	   (case  List.partition satp news  of
    87.7 -		([],nonsats) => next(Library.foldr ThmHeap.insert
    87.8 -					(map pairsize nonsats, nprf_heap)) 
    87.9 +		([],nonsats) => next(foldr ThmHeap.insert
   87.10 +					nprf_heap (map pairsize nonsats))
   87.11  	      | (sats,_)  => some_of_list sats)
   87.12        and next nprf_heap =
   87.13              if ThmHeap.is_empty nprf_heap then NONE
   87.14 @@ -277,7 +277,7 @@
   87.15        let fun cost thm = (level, costf level thm, thm)
   87.16        in (case  List.partition satp news  of
   87.17              ([],nonsats) 
   87.18 -		 => next (Library.foldr insert_with_level (map cost nonsats, nprfs))
   87.19 +		 => next (foldr insert_with_level nprfs (map cost nonsats))
   87.20            | (sats,_)  => some_of_list sats)
   87.21        end and    
   87.22        next []  = NONE
    88.1 --- a/src/Pure/sign.ML	Fri Mar 04 11:44:26 2005 +0100
    88.2 +++ b/src/Pure/sign.ML	Fri Mar 04 15:07:34 2005 +0100
    88.3 @@ -832,7 +832,7 @@
    88.4    let
    88.5      val tsig = tsig_of sg;
    88.6  
    88.7 -    val termss = Library.foldr multiply (map fst args, [[]]);
    88.8 +    val termss = foldr multiply [[]] (map fst args);
    88.9      val typs =
   88.10        map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
   88.11  
    89.1 --- a/src/Pure/tactic.ML	Fri Mar 04 11:44:26 2005 +0100
    89.2 +++ b/src/Pure/tactic.ML	Fri Mar 04 15:07:34 2005 +0100
    89.3 @@ -426,7 +426,7 @@
    89.4  
    89.5  (*build a pair of nets for biresolution*)
    89.6  fun build_netpair netpair brls =
    89.7 -    Library.foldr insert_tagged_brl (taglist 1 brls, netpair);
    89.8 +    foldr insert_tagged_brl netpair (taglist 1 brls);
    89.9  
   89.10  (*delete one kbrl from the pair of nets*)
   89.11  local
   89.12 @@ -473,7 +473,7 @@
   89.13  
   89.14  (*build a net of rules for resolution*)
   89.15  fun build_net rls =
   89.16 -    Library.foldr insert_krl (taglist 1 rls, Net.empty);
   89.17 +    foldr insert_krl Net.empty (taglist 1 rls);
   89.18  
   89.19  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
   89.20  fun filt_resolution_from_net_tac match pred net =
   89.21 @@ -644,7 +644,7 @@
   89.22      val statement = Logic.list_implies (asms, prop);
   89.23      val frees = map Term.dest_Free (Term.term_frees statement);
   89.24      val fixed_frees = filter_out (fn (x, _) => x mem_string xs) frees;
   89.25 -    val fixed_tfrees = Library.foldr Term.add_typ_tfree_names (map #2 fixed_frees, []);
   89.26 +    val fixed_tfrees = foldr Term.add_typ_tfree_names [] (map #2 fixed_frees);
   89.27      val params = List.mapPartial (fn x => Option.map (pair x) (assoc_string (frees, x))) xs;
   89.28  
   89.29      fun err msg = raise ERROR_MESSAGE
    90.1 --- a/src/Pure/tctical.ML	Fri Mar 04 11:44:26 2005 +0100
    90.2 +++ b/src/Pure/tctical.ML	Fri Mar 04 15:07:34 2005 +0100
    90.3 @@ -179,10 +179,10 @@
    90.4  fun EVERY1 tacs = EVERY' tacs 1;
    90.5  
    90.6  (* FIRST [tac1,...,tacn]   equals    tac1 ORELSE ... ORELSE tacn   *)
    90.7 -fun FIRST tacs = Library.foldr (op ORELSE) (tacs, no_tac);
    90.8 +fun FIRST tacs = foldr (op ORELSE) no_tac tacs;
    90.9  
   90.10  (* FIRST' [tac1,...,tacn] i  equals    tac1 i ORELSE ... ORELSE tacn i   *)
   90.11 -fun FIRST' tacs = Library.foldr (op ORELSE') (tacs, K no_tac);
   90.12 +fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs;
   90.13  
   90.14  (*Apply first tactic to 1*)
   90.15  fun FIRST1 tacs = FIRST' tacs 1;
   90.16 @@ -439,7 +439,7 @@
   90.17    let val {sign,maxidx,...} = rep_thm state
   90.18        val cterm = cterm_of sign
   90.19        (*find all vars in the hyps -- should find tvars also!*)
   90.20 -      val hyps_vars = Library.foldr add_term_vars (Logic.strip_assums_hyp prem, [])
   90.21 +      val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem)
   90.22        val insts = map mk_inst hyps_vars
   90.23        (*replace the hyps_vars by Frees*)
   90.24        val prem' = subst_atomic insts prem
   90.25 @@ -472,7 +472,7 @@
   90.26        fun relift st =
   90.27          let val prop = #prop(rep_thm st)
   90.28              val subgoal_vars = (*Vars introduced in the subgoals*)
   90.29 -                  Library.foldr add_term_vars (Logic.strip_imp_prems prop, [])
   90.30 +                  foldr add_term_vars [] (Logic.strip_imp_prems prop)
   90.31              and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
   90.32              val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
   90.33              val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
    91.1 --- a/src/Pure/term.ML	Fri Mar 04 11:44:26 2005 +0100
    91.2 +++ b/src/Pure/term.ML	Fri Mar 04 15:07:34 2005 +0100
    91.3 @@ -773,11 +773,11 @@
    91.4  
    91.5  (** Consts etc. **)
    91.6  
    91.7 -fun add_typ_classes (Type (_, Ts), cs) = Library.foldr add_typ_classes (Ts, cs)
    91.8 +fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
    91.9    | add_typ_classes (TFree (_, S), cs) = S union cs
   91.10    | add_typ_classes (TVar (_, S), cs) = S union cs;
   91.11  
   91.12 -fun add_typ_tycons (Type (c, Ts), cs) = Library.foldr add_typ_tycons (Ts, c ins cs)
   91.13 +fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins cs) Ts
   91.14    | add_typ_tycons (_, cs) = cs;
   91.15  
   91.16  val add_term_classes = it_term_types add_typ_classes;
   91.17 @@ -840,20 +840,20 @@
   91.18    | add_term_names (_, bs) = bs;
   91.19  
   91.20  (*Accumulates the TVars in a type, suppressing duplicates. *)
   91.21 -fun add_typ_tvars(Type(_,Ts),vs) = Library.foldr add_typ_tvars (Ts,vs)
   91.22 +fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
   91.23    | add_typ_tvars(TFree(_),vs) = vs
   91.24    | add_typ_tvars(TVar(v),vs) = v ins vs;
   91.25  
   91.26  (*Accumulates the TFrees in a type, suppressing duplicates. *)
   91.27 -fun add_typ_tfree_names(Type(_,Ts),fs) = Library.foldr add_typ_tfree_names (Ts,fs)
   91.28 +fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
   91.29    | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
   91.30    | add_typ_tfree_names(TVar(_),fs) = fs;
   91.31  
   91.32 -fun add_typ_tfrees(Type(_,Ts),fs) = Library.foldr add_typ_tfrees (Ts,fs)
   91.33 +fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
   91.34    | add_typ_tfrees(TFree(f),fs) = f ins fs
   91.35    | add_typ_tfrees(TVar(_),fs) = fs;
   91.36  
   91.37 -fun add_typ_varnames(Type(_,Ts),nms) = Library.foldr add_typ_varnames (Ts,nms)
   91.38 +fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
   91.39    | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
   91.40    | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
   91.41  
    92.1 --- a/src/Pure/thm.ML	Fri Mar 04 11:44:26 2005 +0100
    92.2 +++ b/src/Pure/thm.ML	Fri Mar 04 15:07:34 2005 +0100
    92.3 @@ -977,8 +977,8 @@
    92.4    No longer normalizes the new theorem! *)
    92.5  fun instantiate ([], []) th = th
    92.6    | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) =
    92.7 -  let val (newsign_ref,tpairs) = Library.foldr add_ctpair (ctpairs, (sign_ref,[]));
    92.8 -      val (newsign_ref,vTs) = Library.foldr add_ctyp (vcTs, (newsign_ref,[]));
    92.9 +  let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs;
   92.10 +      val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs;
   92.11        fun subst t =
   92.12          subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t);
   92.13        val newprop = subst prop;
   92.14 @@ -1041,7 +1041,7 @@
   92.15  (* Replace all TFrees not fixed or in the hyps by new TVars *)
   92.16  fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
   92.17    let
   92.18 -    val tfrees = Library.foldr add_term_tfree_names (hyps, fixed);
   92.19 +    val tfrees = foldr add_term_tfree_names fixed hyps;
   92.20      val prop1 = attach_tpairs tpairs prop;
   92.21      val (prop2, al) = Type.varify (prop1, tfrees);
   92.22      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
   92.23 @@ -1282,8 +1282,8 @@
   92.24    Preserves unknowns in tpairs and on lhs of dpairs. *)
   92.25  fun rename_bvs([],_,_,_) = I
   92.26    | rename_bvs(al,dpairs,tpairs,B) =
   92.27 -    let val vars = Library.foldr add_term_vars
   92.28 -                        (map fst dpairs @ map fst tpairs @ map snd tpairs, [])
   92.29 +    let val vars = foldr add_term_vars []
   92.30 +                        (map fst dpairs @ map fst tpairs @ map snd tpairs)
   92.31          (*unknowns appearing elsewhere be preserved!*)
   92.32          val vids = map (#1 o #1 o dest_Var) vars;
   92.33          fun rename(t as Var((x,i),T)) =
   92.34 @@ -1300,7 +1300,7 @@
   92.35  
   92.36  (*Function to rename bounds/unknowns in the argument, lifted over B*)
   92.37  fun rename_bvars(dpairs, tpairs, B) =
   92.38 -        rename_bvs(Library.foldr Term.match_bvars (dpairs,[]), dpairs, tpairs, B);
   92.39 +        rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
   92.40  
   92.41  
   92.42  (*** RESOLUTION ***)
    93.1 --- a/src/Pure/type.ML	Fri Mar 04 11:44:26 2005 +0100
    93.2 +++ b/src/Pure/type.ML	Fri Mar 04 15:07:34 2005 +0100
    93.3 @@ -252,14 +252,14 @@
    93.4    let
    93.5      val used = add_typ_tfree_names (T, [])
    93.6      and tvars = map #1 (add_typ_tvars (T, []));
    93.7 -    val (alist, _) = Library.foldr new_name (tvars, ([], used));
    93.8 +    val (alist, _) = foldr new_name ([], used) tvars;
    93.9    in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
   93.10  
   93.11  fun freeze_thaw t =
   93.12    let
   93.13      val used = it_term_types add_typ_tfree_names (t, [])
   93.14      and tvars = map #1 (it_term_types add_typ_tvars (t, []));
   93.15 -    val (alist, _) = Library.foldr new_name (tvars, ([], used));
   93.16 +    val (alist, _) = foldr new_name ([], used) tvars;
   93.17    in
   93.18      (case alist of
   93.19        [] => (t, fn x => x) (*nothing to do!*)
   93.20 @@ -378,7 +378,7 @@
   93.21            else meet ((T, S), Vartab.update_new ((v, T), tye))
   93.22        | (Type (a, Ts), Type (b, Us)) =>
   93.23            if a <> b then raise TUNIFY
   93.24 -          else Library.foldr unif (Ts ~~ Us, tye)
   93.25 +          else foldr unif tye (Ts ~~ Us)
   93.26        | (T, U) => if T = U then tye else raise TUNIFY);
   93.27    in (unif (TU, tyenv), ! tyvar_count) end;
   93.28  
    94.1 --- a/src/Pure/unify.ML	Fri Mar 04 11:44:26 2005 +0100
    94.2 +++ b/src/Pure/unify.ML	Fri Mar 04 15:07:34 2005 +0100
    94.3 @@ -291,7 +291,7 @@
    94.4    Clever would be to re-do just the affected dpairs*)
    94.5  fun SIMPL (env,dpairs) : Envir.env * dpair list * dpair list =
    94.6      let val all as (env',flexflex,flexrigid) =
    94.7 -	    Library.foldr SIMPL0 (dpairs, (env,[],[]));
    94.8 +	    foldr SIMPL0 (env,[],[]) dpairs;
    94.9  	val dps = flexrigid@flexflex
   94.10      in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
   94.11         then SIMPL(env',dps) else all
   94.12 @@ -488,7 +488,7 @@
   94.13  	val (Ts,U) = strip_type env T
   94.14  	and js = length ts - 1  downto 0
   94.15  	val args = sort (make_ord arg_less)
   94.16 -		(Library.foldr (change_arg banned) (flexargs (js,ts,Ts), []))
   94.17 +		(foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
   94.18  	val ts' = map (#t) args
   94.19      in
   94.20      if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
   94.21 @@ -521,7 +521,7 @@
   94.22              then  (bnos, (a,T)::newbinder)	(*needed by both: keep*)
   94.23              else  (j::bnos, newbinder);		(*remove*)
   94.24        val indices = 0 upto (length rbinder - 1);
   94.25 -      val (banned,rbin') = Library.foldr add_index (rbinder~~indices, ([],[]));
   94.26 +      val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices);
   94.27        val (env', t') = clean_term banned (env, t);
   94.28        val (env'',u') = clean_term banned (env',u)
   94.29    in  (ff_assign(env'', rbin', t', u'), tpairs)
   94.30 @@ -575,7 +575,7 @@
   94.31  		then print_dpairs "Enter SIMPL" (env,dpairs)  else ();
   94.32  		SIMPL (env,dpairs))
   94.33  	  in case flexrigid of
   94.34 -	      [] => SOME (Library.foldr add_ffpair (flexflex, (env',[])), reseq)
   94.35 +	      [] => SOME (foldr add_ffpair (env',[]) flexflex, reseq)
   94.36  	    | dp::frigid' => 
   94.37  		if tdepth > !search_bound then
   94.38  		    (warning "Unification bound exceeded"; Seq.pull reseq)
   94.39 @@ -626,7 +626,7 @@
   94.40  
   94.41  (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
   94.42  fun smash_flexflex (env,tpairs) : Envir.env =
   94.43 -  Library.foldr smash_flexflex1 (tpairs, env);
   94.44 +  foldr smash_flexflex1 env tpairs;
   94.45  
   94.46  (*Returns unifiers with no remaining disagreement pairs*)
   94.47  fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
    95.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Mar 04 11:44:26 2005 +0100
    95.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Mar 04 15:07:34 2005 +0100
    95.3 @@ -126,11 +126,11 @@
    95.4    (*Treatment of a list of constructors, for one part
    95.5      Result adds a list of terms, each a function variable with arguments*)
    95.6    fun add_case_list (con_ty_list, (opno, case_lists)) =
    95.7 -    let val (opno', case_list) = Library.foldr add_case (con_ty_list, (opno, []))
    95.8 +    let val (opno', case_list) = foldr add_case (opno, []) con_ty_list
    95.9      in (opno', case_list :: case_lists) end;
   95.10  
   95.11    (*Treatment of all parts*)
   95.12 -  val (_, case_lists) = Library.foldr add_case_list (con_ty_lists, (1,[]));
   95.13 +  val (_, case_lists) = foldr add_case_list (1,[]) con_ty_lists;
   95.14  
   95.15    (*extract the types of all the variables*)
   95.16    val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
   95.17 @@ -170,9 +170,9 @@
   95.18            val rec_args = map (make_rec_call (rev case_args,0))
   95.19                           (List.drop(recursor_args, ncase_args))
   95.20        in
   95.21 -          Library.foldr add_abs
   95.22 -            (case_args, list_comb (recursor_var,
   95.23 -                                   bound_args @ rec_args))
   95.24 +          foldr add_abs
   95.25 +            (list_comb (recursor_var,
   95.26 +                        bound_args @ rec_args)) case_args
   95.27        end
   95.28  
   95.29    (*Find each recursive argument and add a recursive call for it*)
   95.30 @@ -202,7 +202,7 @@
   95.31    val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
   95.32  
   95.33    (*Treatment of all parts*)
   95.34 -  val (_, recursor_lists) = Library.foldr add_case_list (rec_ty_lists, (1,[]));
   95.35 +  val (_, recursor_lists) = foldr add_case_list (1,[]) rec_ty_lists;
   95.36  
   95.37    (*extract the types of all the variables*)
   95.38    val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists)
   95.39 @@ -384,7 +384,7 @@
   95.40            (("free_iffs", free_iffs), []),
   95.41            (("free_elims", free_SEs), [])])
   95.42          |> DatatypesData.map (fn tab => Symtab.update ((big_rec_name, dt_info), tab))
   95.43 -        |> ConstructorsData.map (fn tab => Library.foldr Symtab.update (con_pairs, tab))
   95.44 +        |> ConstructorsData.map (fn tab => foldr Symtab.update tab con_pairs)
   95.45          |> Theory.parent_path,
   95.46     ind_result,
   95.47     {con_defs = con_defs,
    96.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Mar 04 11:44:26 2005 +0100
    96.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Mar 04 15:07:34 2005 +0100
    96.3 @@ -178,7 +178,7 @@
    96.4                (Symtab.update
    96.5                 ((big_rec_name, dt_info), DatatypesData.get thy))
    96.6            |> ConstructorsData.put
    96.7 -               (Library.foldr Symtab.update (con_pairs, ConstructorsData.get thy))
    96.8 +               (foldr Symtab.update (ConstructorsData.get thy) con_pairs)
    96.9            |> Theory.parent_path
   96.10    end;
   96.11  
    97.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Mar 04 11:44:26 2005 +0100
    97.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Mar 04 15:07:34 2005 +0100
    97.3 @@ -102,7 +102,7 @@
    97.4                 Sign.string_of_term sign t);
    97.5  
    97.6    (*** Construct the fixedpoint definition ***)
    97.7 -  val mk_variant = variant (Library.foldr add_term_names (intr_tms, []));
    97.8 +  val mk_variant = variant (foldr add_term_names [] intr_tms);
    97.9  
   97.10    val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   97.11  
   97.12 @@ -116,8 +116,8 @@
   97.13          val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds
   97.14          val exfrees = term_frees intr \\ rec_params
   97.15          val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr))
   97.16 -    in Library.foldr FOLogic.mk_exists
   97.17 -             (exfrees, fold_bal FOLogic.mk_conj (zeq::prems))
   97.18 +    in foldr FOLogic.mk_exists
   97.19 +             (fold_bal FOLogic.mk_conj (zeq::prems)) exfrees
   97.20      end;
   97.21  
   97.22    (*The Part(A,h) terms -- compose injections to make h*)
   97.23 @@ -311,8 +311,8 @@
   97.24       (*Make a premise of the induction rule.*)
   97.25       fun induct_prem ind_alist intr =
   97.26         let val quantfrees = map dest_Free (term_frees intr \\ rec_params)
   97.27 -           val iprems = Library.foldr (add_induct_prem ind_alist)
   97.28 -                              (Logic.strip_imp_prems intr,[])
   97.29 +           val iprems = foldr (add_induct_prem ind_alist) []
   97.30 +                              (Logic.strip_imp_prems intr)
   97.31             val (t,X) = Ind_Syntax.rule_concl intr
   97.32             val (SOME pred) = gen_assoc (op aconv) (ind_alist, X)
   97.33             val concl = FOLogic.mk_Trueprop (pred $ t)
   97.34 @@ -390,11 +390,10 @@
   97.35             val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
   97.36                              elem_factors ---> FOLogic.oT)
   97.37             val qconcl =
   97.38 -             Library.foldr FOLogic.mk_all
   97.39 -               (elem_frees,
   97.40 -                FOLogic.imp $
   97.41 +             foldr FOLogic.mk_all
   97.42 +               (FOLogic.imp $
   97.43                  (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
   97.44 -                      $ (list_comb (pfree, elem_frees)))
   97.45 +                      $ (list_comb (pfree, elem_frees))) elem_frees
   97.46         in  (CP.ap_split elem_type FOLogic.oT pfree,
   97.47              qconcl)
   97.48         end;
    98.1 --- a/src/ZF/Tools/primrec_package.ML	Fri Mar 04 11:44:26 2005 +0100
    98.2 +++ b/src/ZF/Tools/primrec_package.ML	Fri Mar 04 15:07:34 2005 +0100
    98.3 @@ -128,7 +128,7 @@
    98.4                | SOME (rhs, cargs', eq) =>
    98.5                      (rhs, inst_recursor (recursor_pair, cargs'), eq)
    98.6            val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
    98.7 -          val abs = Library.foldr absterm (allowed_terms, rhs)
    98.8 +          val abs = foldr absterm rhs allowed_terms
    98.9        in
   98.10            if !Ind_Syntax.trace then
   98.11                writeln ("recursor_rhs = " ^
   98.12 @@ -153,7 +153,7 @@
   98.13      val def_tm = Logic.mk_equals
   98.14                      (subst_bound (rec_arg, fabs),
   98.15                       list_comb (recursor,
   98.16 -                                Library.foldr add_case (cnames ~~ recursor_pairs, []))
   98.17 +                                foldr add_case [] (cnames ~~ recursor_pairs))
   98.18                       $ rec_arg)
   98.19  
   98.20    in
   98.21 @@ -172,7 +172,7 @@
   98.22    let
   98.23      val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args);
   98.24      val SOME (fname, ftype, ls, rs, con_info, eqns) =
   98.25 -      Library.foldr (process_eqn thy) (eqn_terms, NONE);
   98.26 +      foldr (process_eqn thy) NONE eqn_terms;
   98.27      val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
   98.28  
   98.29      val (thy1, [def_thm]) = thy