# HG changeset patch
# User haftmann
# Date 1259080105 -3600
# Node ID fff6f11b1f09584eee96afcac9ec6c3c92e9bee3
# Parent  1bc3b688548c814b81d6be8ab9740e0cb46abb33
curried take/drop

diff -r 1bc3b688548c -r fff6f11b1f09 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/FOLP/simp.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -419,11 +419,11 @@
     if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
     else case Seq.pull(cong_tac i thm) of
             SOME(thm',_) =>
-                    let val ps = prems_of thm and ps' = prems_of thm';
+                    let val ps = prems_of thm
+                        and ps' = prems_of thm';
                         val n = length(ps')-length(ps);
                         val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1)))
-                        val l = map (fn p => length(Logic.strip_assums_hyp(p)))
-                                    (Library.take(n,Library.drop(i-1,ps')));
+                        val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps'));
                     in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
           | NONE => (REW::ss,thm,anet,ats,cs);
 
@@ -535,7 +535,7 @@
 fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
 let fun xn_list(x,n) =
         let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1);
-        in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end
+        in ListPair.map eta_Var (ixs, take (n+1) Ts) end
     val lhs = list_comb(f,xn_list("X",k-1))
     val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
 in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -480,7 +480,7 @@
             then
                 let
                     val paths = Long_Name.explode isa
-                    val i = Library.drop(length paths - 2,paths)
+                    val i = drop (length paths - 2) paths
                 in
                     case i of
                         [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Nov 24 17:28:25 2009 +0100
@@ -130,7 +130,7 @@
 
 fun move_mus i state =
 let val sign = Thm.theory_of_thm state;
-    val (subgoal::_) = Library.drop(i-1,prems_of state);
+    val subgoal = nth (prems_of state) i;
     val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
     val redex = search_mu concl;
     val idx = let val t = #maxidx (rep_thm state) in 
@@ -222,9 +222,9 @@
 (* the interface *)
 
 fun mc_mucke_tac defs i state =
-  (case Library.drop (i - 1, Thm.prems_of state) of
-    [] => no_tac state
-  | subgoal :: _ =>
+  (case try (nth (Thm.prems_of state)) i of
+    NONE => no_tac state
+  | SOME subgoal =>
       EVERY [
         REPEAT (etac thin_rl i),
         cut_facts_tac (mk_lam_defs defs) i,
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -95,7 +95,7 @@
 
 fun if_full_simp_tac sset i state =
 let val sign = Thm.theory_of_thm state;
-        val (subgoal::_) = Library.drop(i-1,prems_of state);
+        val subgoal = nth (prems_of state) i;
         val prems = Logic.strip_imp_prems subgoal;
         val concl = Logic.strip_imp_concl subgoal;
         val prems = prems @ [concl];
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -766,8 +766,8 @@
       Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
 
     val recTs = get_rec_types descr'' sorts;
-    val newTs' = Library.take (length new_type_names, recTs');
-    val newTs = Library.take (length new_type_names, recTs);
+    val newTs' = (uncurry take) (length new_type_names, recTs');
+    val newTs = (uncurry take) (length new_type_names, recTs);
 
     val full_new_type_names = map (Sign.full_bname thy) new_type_names;
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -46,7 +46,7 @@
         val m = length vars and n = length inst;
         val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
         val P :: x :: ys = vars;
-        val zs = Library.drop (m - n - 2, ys);
+        val zs = (uncurry drop) (m - n - 2, ys);
       in
         (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
         (x, tuple (map Free avoiding)) ::
@@ -71,7 +71,7 @@
         val p = length ps;
         val ys =
           if p < n then []
-          else map (tune o #1) (Library.take (p - n, ps)) @ xs;
+          else map (tune o #1) ((uncurry take) (p - n, ps)) @ xs;
       in Logic.list_rename_params (ys, prem) end;
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -328,7 +328,7 @@
        ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
     val unnamed_rules = map (fn induct =>
       ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
-        (Library.drop (length dt_names, inducts));
+        ((uncurry drop) (length dt_names, inducts));
   in
     thy9
     |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -51,7 +51,7 @@
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
 
     val {maxidx, ...} = rep_thm induct;
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
@@ -62,7 +62,7 @@
           Abs ("z", T', Const ("True", T''))) induct_Ps;
         val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
           Var (("P", 0), HOLogic.boolT))
-        val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
+        val insts = (uncurry take) (i, dummyPs) @ (P::((uncurry drop) (i + 1, dummyPs)));
         val cert = cterm_of thy;
         val insts' = (map cert induct_Ps) ~~ (map cert insts);
         val induct' = refl RS ((nth
@@ -98,7 +98,7 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
 
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
@@ -283,7 +283,7 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
     val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
     fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
@@ -306,7 +306,7 @@
               val Ts = map (typ_of_dtyp descr' sorts) cargs;
               val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
               val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
-              val frees = Library.take (length cargs, frees');
+              val frees = (uncurry take) (length cargs, frees');
               val free = mk_Free "f" (Ts ---> T') j
             in
              (free, list_abs_free (map dest_Free frees',
@@ -314,14 +314,14 @@
             end) (constrs ~~ (1 upto length constrs)));
 
           val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
-          val fns = flat (Library.take (i, case_dummy_fns)) @
-            fns2 @ flat (Library.drop (i + 1, case_dummy_fns));
+          val fns = flat ((uncurry take) (i, case_dummy_fns)) @
+            fns2 @ flat ((uncurry drop) (i + 1, case_dummy_fns));
           val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
           val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
           val def = (Binding.name (Long_Name.base_name name ^ "_def"),
             Logic.mk_equals (list_comb (Const (name, caseT), fns1),
-              list_comb (reccomb, (flat (Library.take (i, case_dummy_fns))) @
-                fns2 @ (flat (Library.drop (i + 1, case_dummy_fns))) )));
+              list_comb (reccomb, (flat ((uncurry take) (i, case_dummy_fns))) @
+                fns2 @ (flat ((uncurry drop) (i + 1, case_dummy_fns))) )));
           val ([def_thm], thy') =
             thy
             |> Sign.declare_const decl |> snd
@@ -329,7 +329,7 @@
 
         in (defs @ [def_thm], thy')
         end) (hd descr ~~ newTs ~~ case_names ~~
-          Library.take (length newTs, reccomb_names)) ([], thy1)
+          (uncurry take) (length newTs, reccomb_names)) ([], thy1)
       ||> Theory.checkpoint;
 
     val case_thms = map (map (fn t => Skip_Proof.prove_global thy2 [] [] t
@@ -353,7 +353,7 @@
 
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
 
     fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
         exhaustion), case_thms'), T) =
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -217,18 +217,18 @@
        invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
     else
       let
-        val ts1 = Library.take (i, ts);
-        val t :: ts2 = Library.drop (i, ts);
+        val ts1 = (uncurry take) (i, ts);
+        val t :: ts2 = (uncurry drop) (i, ts);
         val names = List.foldr OldTerm.add_term_names
           (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
-        val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
+        val (Ts, dT) = split_last ((uncurry take) (i+1, fst (strip_type T)));
 
         fun pcase [] [] [] gr = ([], gr)
           | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
               let
                 val j = length cargs;
                 val xs = Name.variant_list names (replicate j "x");
-                val Us' = Library.take (j, fst (strip_type U));
+                val Us' = (uncurry take) (j, fst (strip_type U));
                 val frees = map Free (xs ~~ Us');
                 val (cp, gr0) = invoke_codegen thy defs dep module false
                   (list_comb (Const (cname, Us' ---> dT), frees)) gr;
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Datatype/datatype_prop.ML
--- a/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -72,7 +72,7 @@
         end;
   in
     map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
-      (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
+      (hd descr) ((uncurry take) (length (hd descr), get_rec_types descr' sorts))
   end;
 
 
@@ -82,7 +82,7 @@
   let
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
 
     fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
 
@@ -174,7 +174,7 @@
       end
 
   in map make_casedist
-    ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
+    ((hd descr) ~~ (uncurry take) (length (hd descr), get_rec_types descr' sorts))
   end;
 
 (*************** characteristic equations for primrec combinator **************)
@@ -257,7 +257,7 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
     val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
@@ -280,7 +280,7 @@
   let
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
 
     fun make_case T comb_t ((cname, cargs), f) =
       let
@@ -304,7 +304,7 @@
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
     val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);
 
@@ -415,7 +415,7 @@
   let
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
-    val newTs = Library.take (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
 
     fun mk_eqn T (cname, cargs) =
       let
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -77,8 +77,8 @@
       subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
     val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
     val recTs = get_rec_types descr' sorts;
-    val newTs = Library.take (length (hd descr), recTs);
-    val oldTs = Library.drop (length (hd descr), recTs);
+    val newTs = (uncurry take) (length (hd descr), recTs);
+    val oldTs = (uncurry drop) (length (hd descr), recTs);
     val sumT = if null leafTs then HOLogic.unitT
       else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
     val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
@@ -193,7 +193,7 @@
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
               (resolve_tac rep_intrs 1)))
                 (types_syntax ~~ tyvars ~~
-                  (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
+                  ((uncurry take) (length newTs, rep_set_names)) ~~ new_type_names) ||>
       Sign.add_path big_name;
 
     (*********************** definition of constructors ***********************)
@@ -472,7 +472,7 @@
       iso_inj_thms_unfolded;
 
     val iso_thms = if length descr = 1 then [] else
-      Library.drop (length newTs, split_conj_thm
+      (uncurry drop) (length newTs, split_conj_thm
         (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
            [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
             REPEAT (rtac TrueI 1),
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -121,9 +121,9 @@
                            (Function_Split.split_all_equations ctxt compleqs)
 
           fun restore_spec thms =
-              bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
+              bnds ~~ (uncurry take) (length bnds, Library.unflat spliteqs thms)
               
-          val spliteqs' = flat (Library.take (length bnds, spliteqs))
+          val spliteqs' = flat ((uncurry take) (length bnds, spliteqs))
           val fnames = map (fst o fst) fixes
           val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -899,7 +899,7 @@
   val (qs,p) = isolate_monomials vars eq
   val rs = ideal (qs @ ps) p 
               (fn (s,t) => TermOrd.term_ord (term_of s, term_of t))
- in (eq,Library.take (length qs, rs) ~~ vars)
+ in (eq,(uncurry take) (length qs, rs) ~~ vars)
  end;
  fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
 in
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -655,7 +655,7 @@
               update_checked_problems problems (unsat_js @ map fst lib_ps);
               if null con_ps then
                 let
-                  val num_genuine = Library.take (max_potential, lib_ps)
+                  val num_genuine = take max_potential lib_ps
                                     |> map (print_and_check false)
                                     |> filter (equal (SOME true)) |> length
                   val max_genuine = max_genuine - num_genuine
@@ -689,7 +689,7 @@
                 end
               else
                 let
-                  val _ = Library.take (max_genuine, con_ps)
+                  val _ = take max_genuine con_ps
                           |> List.app (ignore o print_and_check true)
                   val max_genuine = max_genuine - length con_ps
                 in
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -496,7 +496,7 @@
                                   bisim_depths mono_Ts nonmono_Ts
     val ranks = map rank_of_block blocks
     val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
-    val head = Library.take (max_scopes, all)
+    val head = (uncurry take) (max_scopes, all)
     val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
                            head
   in
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -193,8 +193,7 @@
 fun mk_pat (c,l) =
   let val L = length (binder_types (type_of c))
       fun build (prfx,tag,plist) =
-          let val args   = Library.take (L,plist)
-              and plist' = Library.drop(L,plist)
+          let val (args, plist') = chop L plist
           in (prfx,tag,list_comb(c,args)::plist') end
   in map build l end;
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -217,7 +217,7 @@
 fun make_bool_args' xs =
   make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
 
-fun arg_types_of k c = Library.drop (k, binder_types (fastype_of c));
+fun arg_types_of k c = (uncurry drop) (k, binder_types (fastype_of c));
 
 fun find_arg T x [] = sys_error "find_arg"
   | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -67,7 +67,7 @@
     val Tvs = map TVar iTs;
     val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_imp_concl (prop_of (hd intrs))));
-    val params = map dest_Var (Library.take (nparms, ts));
+    val params = map dest_Var ((uncurry take) (nparms, ts));
     val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
     fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
       map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -124,8 +124,8 @@
               let
                 val fnameT' as (fname', _) = dest_Const f;
                 val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
-                val ls = Library.take (rpos, ts);
-                val rest = Library.drop (rpos, ts);
+                val ls = (uncurry take) (rpos, ts);
+                val rest = (uncurry drop) (rpos, ts);
                 val (x', rs) = (hd rest, tl rest)
                   handle Empty => raise RecError ("not enough arguments\
                    \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/record.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -321,7 +321,7 @@
 fun rec_id i T =
   let
     val rTs = dest_recTs T;
-    val rTs' = if i < 0 then rTs else Library.take (i, rTs);
+    val rTs' = if i < 0 then rTs else (uncurry take) (i, rTs);
   in implode (map #1 rTs') end;
 
 
@@ -1582,7 +1582,7 @@
       (Logic.strip_assums_concl (prop_of rule')));
     (*ca indicates if rule is a case analysis or induction rule*)
     val (x, ca) =
-      (case rev (Library.drop (length params, ys)) of
+      (case rev ((uncurry drop) (length params, ys)) of
         [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
           (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
       | [x] => (head_of x, false));
@@ -1635,7 +1635,7 @@
         else if len > 16 then
           let
             fun group16 [] = []
-              | group16 xs = Library.take (16, xs) :: group16 (Library.drop (16, xs));
+              | group16 xs = (uncurry take) (16, xs) :: group16 ((uncurry drop) (16, xs));
             val vars' = group16 vars;
             val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
           in
@@ -1772,7 +1772,7 @@
 
 fun chunks [] [] = []
   | chunks [] xs = [xs]
-  | chunks (l :: ls) xs = Library.take (l, xs) :: chunks ls (Library.drop (l, xs));
+  | chunks (l :: ls) xs = (uncurry take) (l, xs) :: chunks ls ((uncurry drop) (l, xs));
 
 fun chop_last [] = error "chop_last: list should not be empty"
   | chop_last [x] = ([], x)
@@ -1881,12 +1881,12 @@
     val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
     val extension_id = implode extension_names;
 
-    fun rec_schemeT n = mk_recordT (map #extension (Library.drop (n, parents))) extT;
+    fun rec_schemeT n = mk_recordT (map #extension ((uncurry drop) (n, parents))) extT;
     val rec_schemeT0 = rec_schemeT 0;
 
     fun recT n =
       let val (c, Ts) = extension in
-        mk_recordT (map #extension (Library.drop (n, parents)))
+        mk_recordT (map #extension ((uncurry drop) (n, parents)))
           (Type (c, subst_last HOLogic.unitT Ts))
       end;
     val recT0 = recT 0;
@@ -1896,7 +1896,7 @@
         val (args', more) = chop_last args;
         fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
         fun build Ts =
-          fold_rev mk_ext' (Library.drop (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
+          fold_rev mk_ext' ((uncurry drop) (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
             more;
       in
         if more = HOLogic.unit
@@ -1989,7 +1989,7 @@
     val (accessor_thms, updator_thms, upd_acc_cong_assists) =
       timeit_msg "record getting tree access/updates:" get_access_update_thms;
 
-    fun lastN xs = Library.drop (parent_fields_len, xs);
+    fun lastN xs = (uncurry drop) (parent_fields_len, xs);
 
     (*selectors*)
     fun mk_sel_spec ((c, T), thm) =
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -2889,7 +2889,7 @@
               (* go back up the stack until we find a level where we can go *)
               (* to the next sibling node                                   *)
               let
-                val offsets' = Library.dropwhile
+                val offsets' = dropwhile
                   (fn off' => off' mod size_elem = size_elem - 1) offsets
               in
                 case offsets' of
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -74,8 +74,8 @@
       let
         val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
         val (Us', U') = strip_type T;
-        val Us = Library.take (length ts, Us');
-        val U = Library.drop (length ts, Us') ---> U';
+        val Us = (uncurry take) (length ts, Us');
+        val U = (uncurry drop) (length ts, Us') ---> U';
         val T' = maps HOLogic.flatten_tupleT Us ---> U;
         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
               let
diff -r 1bc3b688548c -r fff6f11b1f09 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -153,7 +153,7 @@
     val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-    fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+    fun strip ss = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
     fun typid (Type  (id,_)) =
         let val c = hd (Symbol.explode (Long_Name.base_name id))
         in if Symbol.is_letter c then c else "t" end
@@ -228,7 +228,7 @@
     val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-    fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
+    fun strip ss = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
     fun typid (Type  (id,_)) =
         let val c = hd (Symbol.explode (Long_Name.base_name id))
         in if Symbol.is_letter c then c else "t" end
diff -r 1bc3b688548c -r fff6f11b1f09 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Provers/splitter.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -122,8 +122,8 @@
       fun down [] t i = Bound 0
         | down (p::ps) t i =
             let val (h,ts) = strip_comb t
-                val v1 = ListPair.map var (Library.take(p,ts), i upto (i+p-1))
-                val u::us = Library.drop(p,ts)
+                val v1 = ListPair.map var (take p ts, i upto (i+p-1))
+                val u::us = drop p ts
                 val v2 = ListPair.map var (us, (i+p) upto (i+length(ts)-2))
       in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
   in Abs("", T, down (rev pos) t maxi) end;
@@ -191,7 +191,7 @@
 fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) =
   if n > length ts then []
   else let val lev = length apsns
-           val lbnos = fold add_lbnos (Library.take (n, ts)) []
+           val lbnos = fold add_lbnos (take n ts) []
            val flbnos = filter (fn i => i < lev) lbnos
            val tt = incr_boundvars (~lev) t
        in if null flbnos then
@@ -259,7 +259,7 @@
                 Const(c, cT) =>
                   let fun find [] = []
                         | find ((gcT, pat, thm, T, n)::tups) =
-                            let val t2 = list_comb (h, Library.take (n, ts))
+                            let val t2 = list_comb (h, take n ts)
                             in if Sign.typ_instance sg (cT, gcT)
                                   andalso fomatch sg (Ts,pat,t2)
                                then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/General/path.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -139,7 +139,7 @@
 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
   (case take_suffix (fn c => c <> ".") (explode s) of
     ([], _) => (Path [Basic s], "")
-  | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
+  | (cs, e) => (Path [Basic (implode ((uncurry take) (length cs - 1, cs)))], implode e)));
 
 
 (* expand variables *)
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/General/scan.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -221,7 +221,7 @@
 
 fun trace scan xs =
   let val (y, xs') = scan xs
-  in ((y, Library.take (length xs - length xs', xs)), xs') end;
+  in ((y, (uncurry take) (length xs - length xs', xs)), xs') end;
 
 
 (* stopper *)
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/General/symbol.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -183,7 +183,7 @@
         val raw1 = raw0 o implode;
         val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
     
-        fun encode cs = enc (Library.take_prefix raw_chr cs)
+        fun encode cs = enc (take_prefix raw_chr cs)
         and enc ([], []) = []
           | enc (cs, []) = [raw1 cs]
           | enc ([], d :: ds) = raw2 d :: encode ds
@@ -198,11 +198,11 @@
 
 fun beginning n cs =
   let
-    val drop_blanks = #1 o Library.take_suffix is_ascii_blank;
+    val drop_blanks = #1 o take_suffix is_ascii_blank;
     val all_cs = drop_blanks cs;
     val dots = if length all_cs > n then " ..." else "";
   in
-    (drop_blanks (Library.take (n, all_cs))
+    (drop_blanks (take n all_cs)
       |> map (fn c => if is_ascii_blank c then space else c)
       |> implode) ^ dots
   end;
@@ -491,8 +491,8 @@
 
 fun strip_blanks s =
   sym_explode s
-  |> Library.take_prefix is_blank |> #2
-  |> Library.take_suffix is_blank |> #1
+  |> take_prefix is_blank |> #2
+  |> take_suffix is_blank |> #1
   |> implode;
 
 
@@ -516,7 +516,7 @@
           then chr (ord s + 1) :: ss
           else "a" :: s :: ss;
 
-    val (ss, qs) = apfst rev (Library.take_suffix is_quasi (sym_explode str));
+    val (ss, qs) = apfst rev (take_suffix is_quasi (sym_explode str));
     val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   in implode (rev ss' @ qs) end;
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Isar/code.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -128,7 +128,7 @@
     val args = args_of thm;
     val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
     fun matches_args args' = length args <= length args' andalso
-      Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
+      Pattern.matchess thy (args, (map incr_idx o curry (uncurry take) (length args)) args');
     fun drop (thm', proper') = if (proper orelse not proper')
       andalso matches_args (args_of thm') then 
         (warning ("Code generator: dropping redundant code equation\n" ^
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -232,12 +232,12 @@
         err ("Failed to unify variable " ^
           string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
           string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
-    val (tyenv, _) = fold unify (map #1 vars ~~ Library.take (m, params))
+    val (tyenv, _) = fold unify (map #1 vars ~~ (uncurry take) (m, params))
       (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
     val norm_type = Envir.norm_type tyenv;
 
     val xs = map (apsnd norm_type o fst) vars;
-    val ys = map (apsnd norm_type) (Library.drop (m, params));
+    val ys = map (apsnd norm_type) ((uncurry drop) (m, params));
     val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
     val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -1340,7 +1340,7 @@
       val suppressed = len - ! prems_limit;
       val prt_prems = if null prems then []
         else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
-          map (Display.pretty_thm ctxt) (Library.drop (suppressed, prems)))];
+          map (Display.pretty_thm ctxt) ((uncurry drop) (suppressed, prems)))];
     in prt_structs @ prt_fixes @ prt_prems end;
 
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -144,7 +144,7 @@
           (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
         NONE => (name, NONE)
       | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
-  in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end;
+  in fold_rev add_case ((uncurry drop) (n - nprems, cases)) ([], n) |> #1 end;
 
 in
 
@@ -205,8 +205,8 @@
     th
     |> unfold_prems n defs
     |> unfold_prems_concls defs
-    |> Drule.multi_resolve (Library.take (m, facts))
-    |> Seq.map (pair (xx, (n - m, Library.drop (m, facts))))
+    |> Drule.multi_resolve ((uncurry take) (m, facts))
+    |> Seq.map (pair (xx, (n - m, (uncurry drop) (m, facts))))
   end;
 
 end;
@@ -345,7 +345,7 @@
 fun prep_rule n th =
   let
     val th' = Thm.permute_prems 0 n th;
-    val prems = Library.take (Thm.nprems_of th' - n, Drule.cprems_of th');
+    val prems = (uncurry take) (Thm.nprems_of th' - n, Drule.cprems_of th');
     val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
   in (prems, (n, th'')) end;
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -461,7 +461,7 @@
             end
           else (vs', tye)
 
-      in fold_rev add_args (Library.take (n, vars) ~~ Library.take (n, ts)) ([], []) end;
+      in fold_rev add_args ((uncurry take) (n, vars) ~~ (uncurry take) (n, ts)) ([], []) end;
 
     fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
     fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Syntax/ast.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -158,7 +158,7 @@
       (case (ast, pat) of
         (Appl asts, Appl pats) =>
           let val a = length asts and p = length pats in
-            if a > p then (Appl (Library.take (p, asts)), Library.drop (p, asts))
+            if a > p then (Appl ((uncurry take) (p, asts)), (uncurry drop) (p, asts))
             else (ast, [])
           end
       | _ => (ast, []));
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -499,7 +499,7 @@
         (("Ambiguous input" ^ Position.str_of pos ^
           "\nproduces " ^ string_of_int len ^ " parse trees" ^
           (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-          map show_pt (Library.take (limit, pts)))));
+          map show_pt ((uncurry take) (limit, pts)))));
     SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
   end;
 
@@ -545,7 +545,7 @@
         else cat_error (ambig_msg ()) (cat_lines
           (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
             (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
-            map (Pretty.string_of_term pp) (Library.take (limit, results))))
+            map (Pretty.string_of_term pp) ((uncurry take) (limit, results))))
       end;
 
 fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Thy/present.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -285,7 +285,7 @@
     (browser_info := empty_browser_info; session_info := NONE)
   else
     let
-      val parent_name = name_of_session (Library.take (length path - 1, path));
+      val parent_name = name_of_session ((uncurry take) (length path - 1, path));
       val session_name = name_of_session path;
       val sess_prefix = Path.make path;
       val html_prefix = Path.append (Path.expand output_path) sess_prefix;
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -265,7 +265,7 @@
       if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
       else if nesting >= 0 then (tag', replicate nesting tag @ tags)
       else
-        (case Library.drop (~ nesting - 1, tags) of
+        (case (uncurry drop) (~ nesting - 1, tags) of
           tgs :: tgss => (tgs, tgss)
         | [] => err_bad_nesting (Position.str_of cmd_pos));
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -409,7 +409,7 @@
 
         val len = length matches;
         val lim = the_default (! limit) opt_limit;
-      in (SOME len, Library.drop (len - lim, matches)) end;
+      in (SOME len, (uncurry drop) (len - lim, matches)) end;
 
     val find =
       if rem_dups orelse is_none opt_limit
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/assumption.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -88,12 +88,12 @@
 (* local assumptions *)
 
 fun local_assumptions_of inner outer =
-  Library.drop (length (all_assumptions_of outer), all_assumptions_of inner);
+  (uncurry drop) (length (all_assumptions_of outer), all_assumptions_of inner);
 
 val local_assms_of = maps #2 oo local_assumptions_of;
 
 fun local_prems_of inner outer =
-  Library.drop (length (all_prems_of outer), all_prems_of inner);
+  (uncurry drop) (length (all_prems_of outer), all_prems_of inner);
 
 
 (* add assumptions *)
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/codegen.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -579,11 +579,11 @@
 fun eta_expand t ts i =
   let
     val k = length ts;
-    val Ts = Library.drop (k, binder_types (fastype_of t));
+    val Ts = (uncurry drop) (k, binder_types (fastype_of t));
     val j = i - k
   in
     List.foldr (fn (T, t) => Abs ("x", T, t))
-      (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
+      (list_comb (t, ts @ map Bound (j-1 downto 0))) ((uncurry take) (j, Ts))
   end;
 
 fun mk_app _ p [] = p
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/goal_display.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -99,7 +99,7 @@
       (if main then [prt_term B] else []) @
        (if ngoals = 0 then [Pretty.str "No subgoals!"]
         else if ngoals > maxgoals then
-          pretty_subgoals (Library.take (maxgoals, As)) @
+          pretty_subgoals ((uncurry take) (maxgoals, As)) @
           (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
            else [])
         else pretty_subgoals As) @
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/library.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -81,6 +81,8 @@
   val filter: ('a -> bool) -> 'a list -> 'a list
   val filter_out: ('a -> bool) -> 'a list -> 'a list
   val map_filter: ('a -> 'b option) -> 'a list -> 'b list
+  val take: int -> 'a list -> 'a list
+  val drop: int -> 'a list -> 'a list
   val chop: int -> 'a list -> 'a list * 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
   val nth: 'a list -> int -> 'a
@@ -224,8 +226,6 @@
   val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
-  val take: int * 'a list -> 'a list
-  val drop: int * 'a list -> 'a list
   val last_elem: 'a list -> 'a
 end;
 
@@ -423,20 +423,20 @@
 fun filter_out f = filter (not o f);
 val map_filter = List.mapPartial;
 
+fun take (0: int) xs = []
+  | take _ [] = []
+  | take n (x :: xs) =
+      if n > 0 then x :: take (n - 1) xs else [];
+
+fun drop (0: int) xs = xs
+  | drop _ [] = []
+  | drop n (x :: xs) =
+      if n > 0 then drop (n - 1) xs else x :: xs;
+
 fun chop (0: int) xs = ([], xs)
   | chop _ [] = ([], [])
   | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
 
-(*take the first n elements from a list*)
-fun take (n: int, []) = []
-  | take (n, x :: xs) =
-      if n > 0 then x :: take (n - 1, xs) else [];
-
-(*drop the first n elements from a list*)
-fun drop (n: int, []) = []
-  | drop (n, x :: xs) =
-      if n > 0 then drop (n - 1, xs) else x :: xs;
-
 fun dropwhile P [] = []
   | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/meta_simplifier.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -1163,9 +1163,9 @@
               val (rrs', asm') = rules_of_prem ss prem'
             in mut_impc prems concl rrss asms (prem' :: prems')
               (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
-                (Library.take (i, prems))
+                ((uncurry take) (i, prems))
                 (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
-                  (Library.drop (i, prems), concl))))) :: eqns)
+                  ((uncurry drop) (i, prems), concl))))) :: eqns)
                   ss (length prems') ~1
             end
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/proofterm.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -1003,7 +1003,7 @@
               | _ => error "shrink: proof not in normal form");
             val vs = vars_of prop;
             val (ts', ts'') = chop (length vs) ts;
-            val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
+            val insts = (uncurry take) (length ts', map (fst o dest_Var) vs) ~~ ts';
             val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
               insert (op =) ixn (case AList.lookup (op =) insts ixn of
                   SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/tactic.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -173,7 +173,7 @@
   perm_tac 0 (1 - i);
 
 fun distinct_subgoal_tac i st =
-  (case Library.drop (i - 1, Thm.prems_of st) of
+  (case (uncurry drop) (i - 1, Thm.prems_of st) of
     [] => no_tac st
   | A :: Bs =>
       st |> EVERY (fold (fn (B, k) =>
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/thm.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -1457,7 +1457,7 @@
     val short = length iparams - length cs;
     val newnames =
       if short < 0 then error "More names than abstractions!"
-      else Name.variant_list cs (Library.take (short, iparams)) @ cs;
+      else Name.variant_list cs ((uncurry take) (short, iparams)) @ cs;
     val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
     val newBi = Logic.list_rename_params (newnames, Bi);
   in
diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/variable.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -345,7 +345,7 @@
     val fixes_inner = fixes_of inner;
     val fixes_outer = fixes_of outer;
 
-    val gen_fixes = map #2 (Library.take (length fixes_inner - length fixes_outer, fixes_inner));
+    val gen_fixes = map #2 ((uncurry take) (length fixes_inner - length fixes_outer, fixes_inner));
     val still_fixed = not o member (op =) gen_fixes;
 
     val type_occs_inner = type_occs_of inner;
diff -r 1bc3b688548c -r fff6f11b1f09 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Tools/Code/code_haskell.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -78,7 +78,7 @@
     and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
      of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
       | fingerprint => let
-          val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
+          val ts_fingerprint = ts ~~ curry (uncurry take) (length ts) fingerprint;
           val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
             (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
           fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t
@@ -86,7 +86,7 @@
                 brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty];
         in
           if needs_annotation then
-            (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
+            (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry (uncurry take) (length ts) tys)
           else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
         end
     and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
diff -r 1bc3b688548c -r fff6f11b1f09 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Tools/Code/code_printer.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -231,7 +231,7 @@
    of NONE => brackify fxy (pr_app thm vars app)
     | SOME (k, pr) =>
         let
-          fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry Library.take k tys);
+          fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry (uncurry take) k tys);
         in if k = length ts
           then pr' fxy ts
         else if k < length ts
diff -r 1bc3b688548c -r fff6f11b1f09 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -226,7 +226,7 @@
     val l = k - j;
     val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
     val vs_tys = (map o apfst) SOME
-      (Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys));
+      (Name.names ctxt "a" ((curry (uncurry take) l o curry (uncurry drop) j) tys));
   in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
 
 fun contains_dictvar t =
@@ -773,7 +773,7 @@
         val clauses = if null case_pats
           then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
           else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
-            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry Library.take n tys) t)
+            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry (uncurry take) n tys) t)
               (constrs ~~ ts_clause);
       in ((t, ty), clauses) end;
   in
@@ -788,7 +788,7 @@
   if length ts < num_args then
     let
       val k = length ts;
-      val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
+      val tys = (curry (uncurry take) (num_args - k) o curry (uncurry drop) k o fst o strip_type) ty;
       val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
       val vs = Name.names ctxt "a" tys;
     in
@@ -797,8 +797,8 @@
       #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
     end
   else if length ts > num_args then
-    translate_case thy algbr eqngr thm case_scheme ((c, ty), Library.take (num_args, ts))
-    ##>> fold_map (translate_term thy algbr eqngr thm) (Library.drop (num_args, ts))
+    translate_case thy algbr eqngr thm case_scheme ((c, ty), (uncurry take) (num_args, ts))
+    ##>> fold_map (translate_term thy algbr eqngr thm) ((uncurry drop) (num_args, ts))
     #>> (fn (t, ts) => t `$$ ts)
   else
     translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
diff -r 1bc3b688548c -r fff6f11b1f09 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Tools/induct.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -280,11 +280,11 @@
 
 fun align_left msg xs ys =
   let val m = length xs and n = length ys
-  in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
+  in if m < n then error msg else ((uncurry take) (n, xs) ~~ ys) end;
 
 fun align_right msg xs ys =
   let val m = length xs and n = length ys
-  in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
+  in if m < n then error msg else ((uncurry drop) (m - n, xs) ~~ ys) end;
 
 
 (* prep_inst *)
diff -r 1bc3b688548c -r fff6f11b1f09 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Tools/induct_tacs.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -59,7 +59,7 @@
 
 fun prep_inst (concl, xs) =
   let val vs = Induct.vars_of concl
-  in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
+  in map_filter prep_var ((uncurry drop) (length vs - length xs, vs) ~~ xs) end;
 
 in
 
diff -r 1bc3b688548c -r fff6f11b1f09 src/ZF/Tools/cartprod.ML
--- a/src/ZF/Tools/cartprod.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/ZF/Tools/cartprod.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -97,7 +97,7 @@
 (*Makes a nested tuple from a list, following the product type structure*)
 fun mk_tuple pair (Type("*", [T1,T2])) tms = 
         pair $ (mk_tuple pair T1 tms)
-             $ (mk_tuple pair T2 (Library.drop (length (factors T1), tms)))
+             $ (mk_tuple pair T2 ((uncurry drop) (length (factors T1), tms)))
   | mk_tuple pair T (t::_) = t;
 
 (*Attempts to remove occurrences of split, and pair-valued parameters*)