curried take/drop
authorhaftmann
Tue Nov 24 17:28:25 2009 +0100 (2009-11-24)
changeset 33955fff6f11b1f09
parent 33954 1bc3b688548c
child 33956 6f549f5e7066
curried take/drop
src/FOLP/simp.ML
src/HOL/Import/hol4rews.ML
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/fun.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/split_rule.ML
src/HOLCF/Tools/Domain/domain_extender.ML
src/Provers/splitter.ML
src/Pure/General/path.ML
src/Pure/General/scan.ML
src/Pure/General/symbol.ML
src/Pure/Isar/code.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Proof/extraction.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/find_theorems.ML
src/Pure/assumption.ML
src/Pure/codegen.ML
src/Pure/goal_display.ML
src/Pure/library.ML
src/Pure/meta_simplifier.ML
src/Pure/proofterm.ML
src/Pure/tactic.ML
src/Pure/thm.ML
src/Pure/variable.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_thingol.ML
src/Tools/induct.ML
src/Tools/induct_tacs.ML
src/ZF/Tools/cartprod.ML
     1.1 --- a/src/FOLP/simp.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/FOLP/simp.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -419,11 +419,11 @@
     1.4      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
     1.5      else case Seq.pull(cong_tac i thm) of
     1.6              SOME(thm',_) =>
     1.7 -                    let val ps = prems_of thm and ps' = prems_of thm';
     1.8 +                    let val ps = prems_of thm
     1.9 +                        and ps' = prems_of thm';
    1.10                          val n = length(ps')-length(ps);
    1.11                          val a = length(Logic.strip_assums_hyp(List.nth(ps,i-1)))
    1.12 -                        val l = map (fn p => length(Logic.strip_assums_hyp(p)))
    1.13 -                                    (Library.take(n,Library.drop(i-1,ps')));
    1.14 +                        val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps'));
    1.15                      in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
    1.16            | NONE => (REW::ss,thm,anet,ats,cs);
    1.17  
    1.18 @@ -535,7 +535,7 @@
    1.19  fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
    1.20  let fun xn_list(x,n) =
    1.21          let val ixs = map_range (fn i => (x^(radixstring(26,"a",i)),0)) (n - 1);
    1.22 -        in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end
    1.23 +        in ListPair.map eta_Var (ixs, take (n+1) Ts) end
    1.24      val lhs = list_comb(f,xn_list("X",k-1))
    1.25      val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
    1.26  in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
     2.1 --- a/src/HOL/Import/hol4rews.ML	Tue Nov 24 14:37:23 2009 +0100
     2.2 +++ b/src/HOL/Import/hol4rews.ML	Tue Nov 24 17:28:25 2009 +0100
     2.3 @@ -480,7 +480,7 @@
     2.4              then
     2.5                  let
     2.6                      val paths = Long_Name.explode isa
     2.7 -                    val i = Library.drop(length paths - 2,paths)
     2.8 +                    val i = drop (length paths - 2) paths
     2.9                  in
    2.10                      case i of
    2.11                          [seg,con] => output_thy ^ "." ^ seg ^ "." ^ con
     3.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Nov 24 14:37:23 2009 +0100
     3.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Nov 24 17:28:25 2009 +0100
     3.3 @@ -130,7 +130,7 @@
     3.4  
     3.5  fun move_mus i state =
     3.6  let val sign = Thm.theory_of_thm state;
     3.7 -    val (subgoal::_) = Library.drop(i-1,prems_of state);
     3.8 +    val subgoal = nth (prems_of state) i;
     3.9      val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
    3.10      val redex = search_mu concl;
    3.11      val idx = let val t = #maxidx (rep_thm state) in 
    3.12 @@ -222,9 +222,9 @@
    3.13  (* the interface *)
    3.14  
    3.15  fun mc_mucke_tac defs i state =
    3.16 -  (case Library.drop (i - 1, Thm.prems_of state) of
    3.17 -    [] => no_tac state
    3.18 -  | subgoal :: _ =>
    3.19 +  (case try (nth (Thm.prems_of state)) i of
    3.20 +    NONE => no_tac state
    3.21 +  | SOME subgoal =>
    3.22        EVERY [
    3.23          REPEAT (etac thin_rl i),
    3.24          cut_facts_tac (mk_lam_defs defs) i,
     4.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Nov 24 14:37:23 2009 +0100
     4.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Nov 24 17:28:25 2009 +0100
     4.3 @@ -95,7 +95,7 @@
     4.4  
     4.5  fun if_full_simp_tac sset i state =
     4.6  let val sign = Thm.theory_of_thm state;
     4.7 -        val (subgoal::_) = Library.drop(i-1,prems_of state);
     4.8 +        val subgoal = nth (prems_of state) i;
     4.9          val prems = Logic.strip_imp_prems subgoal;
    4.10          val concl = Logic.strip_imp_concl subgoal;
    4.11          val prems = prems @ [concl];
     5.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Nov 24 14:37:23 2009 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Nov 24 17:28:25 2009 +0100
     5.3 @@ -766,8 +766,8 @@
     5.4        Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
     5.5  
     5.6      val recTs = get_rec_types descr'' sorts;
     5.7 -    val newTs' = Library.take (length new_type_names, recTs');
     5.8 -    val newTs = Library.take (length new_type_names, recTs);
     5.9 +    val newTs' = (uncurry take) (length new_type_names, recTs');
    5.10 +    val newTs = (uncurry take) (length new_type_names, recTs);
    5.11  
    5.12      val full_new_type_names = map (Sign.full_bname thy) new_type_names;
    5.13  
     6.1 --- a/src/HOL/Nominal/nominal_induct.ML	Tue Nov 24 14:37:23 2009 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Tue Nov 24 17:28:25 2009 +0100
     6.3 @@ -46,7 +46,7 @@
     6.4          val m = length vars and n = length inst;
     6.5          val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
     6.6          val P :: x :: ys = vars;
     6.7 -        val zs = Library.drop (m - n - 2, ys);
     6.8 +        val zs = (uncurry drop) (m - n - 2, ys);
     6.9        in
    6.10          (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
    6.11          (x, tuple (map Free avoiding)) ::
    6.12 @@ -71,7 +71,7 @@
    6.13          val p = length ps;
    6.14          val ys =
    6.15            if p < n then []
    6.16 -          else map (tune o #1) (Library.take (p - n, ps)) @ xs;
    6.17 +          else map (tune o #1) ((uncurry take) (p - n, ps)) @ xs;
    6.18        in Logic.list_rename_params (ys, prem) end;
    6.19      fun rename_prems prop =
    6.20        let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
     7.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Nov 24 14:37:23 2009 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Nov 24 17:28:25 2009 +0100
     7.3 @@ -328,7 +328,7 @@
     7.4         ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
     7.5      val unnamed_rules = map (fn induct =>
     7.6        ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
     7.7 -        (Library.drop (length dt_names, inducts));
     7.8 +        ((uncurry drop) (length dt_names, inducts));
     7.9    in
    7.10      thy9
    7.11      |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
     8.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Nov 24 14:37:23 2009 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Nov 24 17:28:25 2009 +0100
     8.3 @@ -51,7 +51,7 @@
     8.4  
     8.5      val descr' = flat descr;
     8.6      val recTs = get_rec_types descr' sorts;
     8.7 -    val newTs = Library.take (length (hd descr), recTs);
     8.8 +    val newTs = (uncurry take) (length (hd descr), recTs);
     8.9  
    8.10      val {maxidx, ...} = rep_thm induct;
    8.11      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    8.12 @@ -62,7 +62,7 @@
    8.13            Abs ("z", T', Const ("True", T''))) induct_Ps;
    8.14          val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
    8.15            Var (("P", 0), HOLogic.boolT))
    8.16 -        val insts = Library.take (i, dummyPs) @ (P::(Library.drop (i + 1, dummyPs)));
    8.17 +        val insts = (uncurry take) (i, dummyPs) @ (P::((uncurry drop) (i + 1, dummyPs)));
    8.18          val cert = cterm_of thy;
    8.19          val insts' = (map cert induct_Ps) ~~ (map cert insts);
    8.20          val induct' = refl RS ((nth
    8.21 @@ -98,7 +98,7 @@
    8.22      val descr' = flat descr;
    8.23      val recTs = get_rec_types descr' sorts;
    8.24      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    8.25 -    val newTs = Library.take (length (hd descr), recTs);
    8.26 +    val newTs = (uncurry take) (length (hd descr), recTs);
    8.27  
    8.28      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    8.29  
    8.30 @@ -283,7 +283,7 @@
    8.31      val descr' = flat descr;
    8.32      val recTs = get_rec_types descr' sorts;
    8.33      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
    8.34 -    val newTs = Library.take (length (hd descr), recTs);
    8.35 +    val newTs = (uncurry take) (length (hd descr), recTs);
    8.36      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
    8.37  
    8.38      fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
    8.39 @@ -306,7 +306,7 @@
    8.40                val Ts = map (typ_of_dtyp descr' sorts) cargs;
    8.41                val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
    8.42                val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
    8.43 -              val frees = Library.take (length cargs, frees');
    8.44 +              val frees = (uncurry take) (length cargs, frees');
    8.45                val free = mk_Free "f" (Ts ---> T') j
    8.46              in
    8.47               (free, list_abs_free (map dest_Free frees',
    8.48 @@ -314,14 +314,14 @@
    8.49              end) (constrs ~~ (1 upto length constrs)));
    8.50  
    8.51            val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
    8.52 -          val fns = flat (Library.take (i, case_dummy_fns)) @
    8.53 -            fns2 @ flat (Library.drop (i + 1, case_dummy_fns));
    8.54 +          val fns = flat ((uncurry take) (i, case_dummy_fns)) @
    8.55 +            fns2 @ flat ((uncurry drop) (i + 1, case_dummy_fns));
    8.56            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
    8.57            val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
    8.58            val def = (Binding.name (Long_Name.base_name name ^ "_def"),
    8.59              Logic.mk_equals (list_comb (Const (name, caseT), fns1),
    8.60 -              list_comb (reccomb, (flat (Library.take (i, case_dummy_fns))) @
    8.61 -                fns2 @ (flat (Library.drop (i + 1, case_dummy_fns))) )));
    8.62 +              list_comb (reccomb, (flat ((uncurry take) (i, case_dummy_fns))) @
    8.63 +                fns2 @ (flat ((uncurry drop) (i + 1, case_dummy_fns))) )));
    8.64            val ([def_thm], thy') =
    8.65              thy
    8.66              |> Sign.declare_const decl |> snd
    8.67 @@ -329,7 +329,7 @@
    8.68  
    8.69          in (defs @ [def_thm], thy')
    8.70          end) (hd descr ~~ newTs ~~ case_names ~~
    8.71 -          Library.take (length newTs, reccomb_names)) ([], thy1)
    8.72 +          (uncurry take) (length newTs, reccomb_names)) ([], thy1)
    8.73        ||> Theory.checkpoint;
    8.74  
    8.75      val case_thms = map (map (fn t => Skip_Proof.prove_global thy2 [] [] t
    8.76 @@ -353,7 +353,7 @@
    8.77  
    8.78      val descr' = flat descr;
    8.79      val recTs = get_rec_types descr' sorts;
    8.80 -    val newTs = Library.take (length (hd descr), recTs);
    8.81 +    val newTs = (uncurry take) (length (hd descr), recTs);
    8.82  
    8.83      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
    8.84          exhaustion), case_thms'), T) =
     9.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 24 14:37:23 2009 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 24 17:28:25 2009 +0100
     9.3 @@ -217,18 +217,18 @@
     9.4         invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
     9.5      else
     9.6        let
     9.7 -        val ts1 = Library.take (i, ts);
     9.8 -        val t :: ts2 = Library.drop (i, ts);
     9.9 +        val ts1 = (uncurry take) (i, ts);
    9.10 +        val t :: ts2 = (uncurry drop) (i, ts);
    9.11          val names = List.foldr OldTerm.add_term_names
    9.12            (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
    9.13 -        val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
    9.14 +        val (Ts, dT) = split_last ((uncurry take) (i+1, fst (strip_type T)));
    9.15  
    9.16          fun pcase [] [] [] gr = ([], gr)
    9.17            | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
    9.18                let
    9.19                  val j = length cargs;
    9.20                  val xs = Name.variant_list names (replicate j "x");
    9.21 -                val Us' = Library.take (j, fst (strip_type U));
    9.22 +                val Us' = (uncurry take) (j, fst (strip_type U));
    9.23                  val frees = map Free (xs ~~ Us');
    9.24                  val (cp, gr0) = invoke_codegen thy defs dep module false
    9.25                    (list_comb (Const (cname, Us' ---> dT), frees)) gr;
    10.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 24 14:37:23 2009 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Tue Nov 24 17:28:25 2009 +0100
    10.3 @@ -72,7 +72,7 @@
    10.4          end;
    10.5    in
    10.6      map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
    10.7 -      (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
    10.8 +      (hd descr) ((uncurry take) (length (hd descr), get_rec_types descr' sorts))
    10.9    end;
   10.10  
   10.11  
   10.12 @@ -82,7 +82,7 @@
   10.13    let
   10.14      val descr' = flat descr;
   10.15      val recTs = get_rec_types descr' sorts;
   10.16 -    val newTs = Library.take (length (hd descr), recTs);
   10.17 +    val newTs = (uncurry take) (length (hd descr), recTs);
   10.18  
   10.19      fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
   10.20  
   10.21 @@ -174,7 +174,7 @@
   10.22        end
   10.23  
   10.24    in map make_casedist
   10.25 -    ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
   10.26 +    ((hd descr) ~~ (uncurry take) (length (hd descr), get_rec_types descr' sorts))
   10.27    end;
   10.28  
   10.29  (*************** characteristic equations for primrec combinator **************)
   10.30 @@ -257,7 +257,7 @@
   10.31      val descr' = flat descr;
   10.32      val recTs = get_rec_types descr' sorts;
   10.33      val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   10.34 -    val newTs = Library.take (length (hd descr), recTs);
   10.35 +    val newTs = (uncurry take) (length (hd descr), recTs);
   10.36      val T' = TFree (Name.variant used "'t", HOLogic.typeS);
   10.37  
   10.38      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   10.39 @@ -280,7 +280,7 @@
   10.40    let
   10.41      val descr' = flat descr;
   10.42      val recTs = get_rec_types descr' sorts;
   10.43 -    val newTs = Library.take (length (hd descr), recTs);
   10.44 +    val newTs = (uncurry take) (length (hd descr), recTs);
   10.45  
   10.46      fun make_case T comb_t ((cname, cargs), f) =
   10.47        let
   10.48 @@ -304,7 +304,7 @@
   10.49      val descr' = flat descr;
   10.50      val recTs = get_rec_types descr' sorts;
   10.51      val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
   10.52 -    val newTs = Library.take (length (hd descr), recTs);
   10.53 +    val newTs = (uncurry take) (length (hd descr), recTs);
   10.54      val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
   10.55      val P = Free ("P", T' --> HOLogic.boolT);
   10.56  
   10.57 @@ -415,7 +415,7 @@
   10.58    let
   10.59      val descr' = flat descr;
   10.60      val recTs = get_rec_types descr' sorts;
   10.61 -    val newTs = Library.take (length (hd descr), recTs);
   10.62 +    val newTs = (uncurry take) (length (hd descr), recTs);
   10.63  
   10.64      fun mk_eqn T (cname, cargs) =
   10.65        let
    11.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Nov 24 14:37:23 2009 +0100
    11.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Nov 24 17:28:25 2009 +0100
    11.3 @@ -77,8 +77,8 @@
    11.4        subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
    11.5      val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
    11.6      val recTs = get_rec_types descr' sorts;
    11.7 -    val newTs = Library.take (length (hd descr), recTs);
    11.8 -    val oldTs = Library.drop (length (hd descr), recTs);
    11.9 +    val newTs = (uncurry take) (length (hd descr), recTs);
   11.10 +    val oldTs = (uncurry drop) (length (hd descr), recTs);
   11.11      val sumT = if null leafTs then HOLogic.unitT
   11.12        else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
   11.13      val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
   11.14 @@ -193,7 +193,7 @@
   11.15                QUIET_BREADTH_FIRST (has_fewer_prems 1)
   11.16                (resolve_tac rep_intrs 1)))
   11.17                  (types_syntax ~~ tyvars ~~
   11.18 -                  (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
   11.19 +                  ((uncurry take) (length newTs, rep_set_names)) ~~ new_type_names) ||>
   11.20        Sign.add_path big_name;
   11.21  
   11.22      (*********************** definition of constructors ***********************)
   11.23 @@ -472,7 +472,7 @@
   11.24        iso_inj_thms_unfolded;
   11.25  
   11.26      val iso_thms = if length descr = 1 then [] else
   11.27 -      Library.drop (length newTs, split_conj_thm
   11.28 +      (uncurry drop) (length newTs, split_conj_thm
   11.29          (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
   11.30             [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
   11.31              REPEAT (rtac TrueI 1),
    12.1 --- a/src/HOL/Tools/Function/fun.ML	Tue Nov 24 14:37:23 2009 +0100
    12.2 +++ b/src/HOL/Tools/Function/fun.ML	Tue Nov 24 17:28:25 2009 +0100
    12.3 @@ -121,9 +121,9 @@
    12.4                             (Function_Split.split_all_equations ctxt compleqs)
    12.5  
    12.6            fun restore_spec thms =
    12.7 -              bnds ~~ Library.take (length bnds, Library.unflat spliteqs thms)
    12.8 +              bnds ~~ (uncurry take) (length bnds, Library.unflat spliteqs thms)
    12.9                
   12.10 -          val spliteqs' = flat (Library.take (length bnds, spliteqs))
   12.11 +          val spliteqs' = flat ((uncurry take) (length bnds, spliteqs))
   12.12            val fnames = map (fst o fst) fixes
   12.13            val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
   12.14  
    13.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Nov 24 14:37:23 2009 +0100
    13.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Nov 24 17:28:25 2009 +0100
    13.3 @@ -899,7 +899,7 @@
    13.4    val (qs,p) = isolate_monomials vars eq
    13.5    val rs = ideal (qs @ ps) p 
    13.6                (fn (s,t) => TermOrd.term_ord (term_of s, term_of t))
    13.7 - in (eq,Library.take (length qs, rs) ~~ vars)
    13.8 + in (eq,(uncurry take) (length qs, rs) ~~ vars)
    13.9   end;
   13.10   fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
   13.11  in
    14.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 24 14:37:23 2009 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 24 17:28:25 2009 +0100
    14.3 @@ -655,7 +655,7 @@
    14.4                update_checked_problems problems (unsat_js @ map fst lib_ps);
    14.5                if null con_ps then
    14.6                  let
    14.7 -                  val num_genuine = Library.take (max_potential, lib_ps)
    14.8 +                  val num_genuine = take max_potential lib_ps
    14.9                                      |> map (print_and_check false)
   14.10                                      |> filter (equal (SOME true)) |> length
   14.11                    val max_genuine = max_genuine - num_genuine
   14.12 @@ -689,7 +689,7 @@
   14.13                  end
   14.14                else
   14.15                  let
   14.16 -                  val _ = Library.take (max_genuine, con_ps)
   14.17 +                  val _ = take max_genuine con_ps
   14.18                            |> List.app (ignore o print_and_check true)
   14.19                    val max_genuine = max_genuine - length con_ps
   14.20                  in
    15.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Nov 24 14:37:23 2009 +0100
    15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Nov 24 17:28:25 2009 +0100
    15.3 @@ -496,7 +496,7 @@
    15.4                                    bisim_depths mono_Ts nonmono_Ts
    15.5      val ranks = map rank_of_block blocks
    15.6      val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
    15.7 -    val head = Library.take (max_scopes, all)
    15.8 +    val head = (uncurry take) (max_scopes, all)
    15.9      val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
   15.10                             head
   15.11    in
    16.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Nov 24 14:37:23 2009 +0100
    16.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Tue Nov 24 17:28:25 2009 +0100
    16.3 @@ -193,8 +193,7 @@
    16.4  fun mk_pat (c,l) =
    16.5    let val L = length (binder_types (type_of c))
    16.6        fun build (prfx,tag,plist) =
    16.7 -          let val args   = Library.take (L,plist)
    16.8 -              and plist' = Library.drop(L,plist)
    16.9 +          let val (args, plist') = chop L plist
   16.10            in (prfx,tag,list_comb(c,args)::plist') end
   16.11    in map build l end;
   16.12  
    17.1 --- a/src/HOL/Tools/inductive.ML	Tue Nov 24 14:37:23 2009 +0100
    17.2 +++ b/src/HOL/Tools/inductive.ML	Tue Nov 24 17:28:25 2009 +0100
    17.3 @@ -217,7 +217,7 @@
    17.4  fun make_bool_args' xs =
    17.5    make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
    17.6  
    17.7 -fun arg_types_of k c = Library.drop (k, binder_types (fastype_of c));
    17.8 +fun arg_types_of k c = (uncurry drop) (k, binder_types (fastype_of c));
    17.9  
   17.10  fun find_arg T x [] = sys_error "find_arg"
   17.11    | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
    18.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Nov 24 14:37:23 2009 +0100
    18.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Nov 24 17:28:25 2009 +0100
    18.3 @@ -67,7 +67,7 @@
    18.4      val Tvs = map TVar iTs;
    18.5      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
    18.6        (Logic.strip_imp_concl (prop_of (hd intrs))));
    18.7 -    val params = map dest_Var (Library.take (nparms, ts));
    18.8 +    val params = map dest_Var ((uncurry take) (nparms, ts));
    18.9      val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
   18.10      fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
   18.11        map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
    19.1 --- a/src/HOL/Tools/old_primrec.ML	Tue Nov 24 14:37:23 2009 +0100
    19.2 +++ b/src/HOL/Tools/old_primrec.ML	Tue Nov 24 17:28:25 2009 +0100
    19.3 @@ -124,8 +124,8 @@
    19.4                let
    19.5                  val fnameT' as (fname', _) = dest_Const f;
    19.6                  val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
    19.7 -                val ls = Library.take (rpos, ts);
    19.8 -                val rest = Library.drop (rpos, ts);
    19.9 +                val ls = (uncurry take) (rpos, ts);
   19.10 +                val rest = (uncurry drop) (rpos, ts);
   19.11                  val (x', rs) = (hd rest, tl rest)
   19.12                    handle Empty => raise RecError ("not enough arguments\
   19.13                     \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
    20.1 --- a/src/HOL/Tools/record.ML	Tue Nov 24 14:37:23 2009 +0100
    20.2 +++ b/src/HOL/Tools/record.ML	Tue Nov 24 17:28:25 2009 +0100
    20.3 @@ -321,7 +321,7 @@
    20.4  fun rec_id i T =
    20.5    let
    20.6      val rTs = dest_recTs T;
    20.7 -    val rTs' = if i < 0 then rTs else Library.take (i, rTs);
    20.8 +    val rTs' = if i < 0 then rTs else (uncurry take) (i, rTs);
    20.9    in implode (map #1 rTs') end;
   20.10  
   20.11  
   20.12 @@ -1582,7 +1582,7 @@
   20.13        (Logic.strip_assums_concl (prop_of rule')));
   20.14      (*ca indicates if rule is a case analysis or induction rule*)
   20.15      val (x, ca) =
   20.16 -      (case rev (Library.drop (length params, ys)) of
   20.17 +      (case rev ((uncurry drop) (length params, ys)) of
   20.18          [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
   20.19            (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
   20.20        | [x] => (head_of x, false));
   20.21 @@ -1635,7 +1635,7 @@
   20.22          else if len > 16 then
   20.23            let
   20.24              fun group16 [] = []
   20.25 -              | group16 xs = Library.take (16, xs) :: group16 (Library.drop (16, xs));
   20.26 +              | group16 xs = (uncurry take) (16, xs) :: group16 ((uncurry drop) (16, xs));
   20.27              val vars' = group16 vars;
   20.28              val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
   20.29            in
   20.30 @@ -1772,7 +1772,7 @@
   20.31  
   20.32  fun chunks [] [] = []
   20.33    | chunks [] xs = [xs]
   20.34 -  | chunks (l :: ls) xs = Library.take (l, xs) :: chunks ls (Library.drop (l, xs));
   20.35 +  | chunks (l :: ls) xs = (uncurry take) (l, xs) :: chunks ls ((uncurry drop) (l, xs));
   20.36  
   20.37  fun chop_last [] = error "chop_last: list should not be empty"
   20.38    | chop_last [x] = ([], x)
   20.39 @@ -1881,12 +1881,12 @@
   20.40      val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
   20.41      val extension_id = implode extension_names;
   20.42  
   20.43 -    fun rec_schemeT n = mk_recordT (map #extension (Library.drop (n, parents))) extT;
   20.44 +    fun rec_schemeT n = mk_recordT (map #extension ((uncurry drop) (n, parents))) extT;
   20.45      val rec_schemeT0 = rec_schemeT 0;
   20.46  
   20.47      fun recT n =
   20.48        let val (c, Ts) = extension in
   20.49 -        mk_recordT (map #extension (Library.drop (n, parents)))
   20.50 +        mk_recordT (map #extension ((uncurry drop) (n, parents)))
   20.51            (Type (c, subst_last HOLogic.unitT Ts))
   20.52        end;
   20.53      val recT0 = recT 0;
   20.54 @@ -1896,7 +1896,7 @@
   20.55          val (args', more) = chop_last args;
   20.56          fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
   20.57          fun build Ts =
   20.58 -          fold_rev mk_ext' (Library.drop (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
   20.59 +          fold_rev mk_ext' ((uncurry drop) (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
   20.60              more;
   20.61        in
   20.62          if more = HOLogic.unit
   20.63 @@ -1989,7 +1989,7 @@
   20.64      val (accessor_thms, updator_thms, upd_acc_cong_assists) =
   20.65        timeit_msg "record getting tree access/updates:" get_access_update_thms;
   20.66  
   20.67 -    fun lastN xs = Library.drop (parent_fields_len, xs);
   20.68 +    fun lastN xs = (uncurry drop) (parent_fields_len, xs);
   20.69  
   20.70      (*selectors*)
   20.71      fun mk_sel_spec ((c, T), thm) =
    21.1 --- a/src/HOL/Tools/refute.ML	Tue Nov 24 14:37:23 2009 +0100
    21.2 +++ b/src/HOL/Tools/refute.ML	Tue Nov 24 17:28:25 2009 +0100
    21.3 @@ -2889,7 +2889,7 @@
    21.4                (* go back up the stack until we find a level where we can go *)
    21.5                (* to the next sibling node                                   *)
    21.6                let
    21.7 -                val offsets' = Library.dropwhile
    21.8 +                val offsets' = dropwhile
    21.9                    (fn off' => off' mod size_elem = size_elem - 1) offsets
   21.10                in
   21.11                  case offsets' of
    22.1 --- a/src/HOL/Tools/split_rule.ML	Tue Nov 24 14:37:23 2009 +0100
    22.2 +++ b/src/HOL/Tools/split_rule.ML	Tue Nov 24 17:28:25 2009 +0100
    22.3 @@ -74,8 +74,8 @@
    22.4        let
    22.5          val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
    22.6          val (Us', U') = strip_type T;
    22.7 -        val Us = Library.take (length ts, Us');
    22.8 -        val U = Library.drop (length ts, Us') ---> U';
    22.9 +        val Us = (uncurry take) (length ts, Us');
   22.10 +        val U = (uncurry drop) (length ts, Us') ---> U';
   22.11          val T' = maps HOLogic.flatten_tupleT Us ---> U;
   22.12          fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
   22.13                let
    23.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Nov 24 14:37:23 2009 +0100
    23.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Nov 24 17:28:25 2009 +0100
    23.3 @@ -153,7 +153,7 @@
    23.4      val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
    23.5      val dts  = map (Type o fst) eqs';
    23.6      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
    23.7 -    fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
    23.8 +    fun strip ss = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
    23.9      fun typid (Type  (id,_)) =
   23.10          let val c = hd (Symbol.explode (Long_Name.base_name id))
   23.11          in if Symbol.is_letter c then c else "t" end
   23.12 @@ -228,7 +228,7 @@
   23.13      val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
   23.14      val dts  = map (Type o fst) eqs';
   23.15      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
   23.16 -    fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
   23.17 +    fun strip ss = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
   23.18      fun typid (Type  (id,_)) =
   23.19          let val c = hd (Symbol.explode (Long_Name.base_name id))
   23.20          in if Symbol.is_letter c then c else "t" end
    24.1 --- a/src/Provers/splitter.ML	Tue Nov 24 14:37:23 2009 +0100
    24.2 +++ b/src/Provers/splitter.ML	Tue Nov 24 17:28:25 2009 +0100
    24.3 @@ -122,8 +122,8 @@
    24.4        fun down [] t i = Bound 0
    24.5          | down (p::ps) t i =
    24.6              let val (h,ts) = strip_comb t
    24.7 -                val v1 = ListPair.map var (Library.take(p,ts), i upto (i+p-1))
    24.8 -                val u::us = Library.drop(p,ts)
    24.9 +                val v1 = ListPair.map var (take p ts, i upto (i+p-1))
   24.10 +                val u::us = drop p ts
   24.11                  val v2 = ListPair.map var (us, (i+p) upto (i+length(ts)-2))
   24.12        in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;
   24.13    in Abs("", T, down (rev pos) t maxi) end;
   24.14 @@ -191,7 +191,7 @@
   24.15  fun mk_split_pack (thm, T: typ, T', n, ts, apsns, pos, TB, t) =
   24.16    if n > length ts then []
   24.17    else let val lev = length apsns
   24.18 -           val lbnos = fold add_lbnos (Library.take (n, ts)) []
   24.19 +           val lbnos = fold add_lbnos (take n ts) []
   24.20             val flbnos = filter (fn i => i < lev) lbnos
   24.21             val tt = incr_boundvars (~lev) t
   24.22         in if null flbnos then
   24.23 @@ -259,7 +259,7 @@
   24.24                  Const(c, cT) =>
   24.25                    let fun find [] = []
   24.26                          | find ((gcT, pat, thm, T, n)::tups) =
   24.27 -                            let val t2 = list_comb (h, Library.take (n, ts))
   24.28 +                            let val t2 = list_comb (h, take n ts)
   24.29                              in if Sign.typ_instance sg (cT, gcT)
   24.30                                    andalso fomatch sg (Ts,pat,t2)
   24.31                                 then mk_split_pack(thm,T,T',n,ts,apsns,pos,type_of1(Ts,t2),t2)
    25.1 --- a/src/Pure/General/path.ML	Tue Nov 24 14:37:23 2009 +0100
    25.2 +++ b/src/Pure/General/path.ML	Tue Nov 24 17:28:25 2009 +0100
    25.3 @@ -139,7 +139,7 @@
    25.4  val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
    25.5    (case take_suffix (fn c => c <> ".") (explode s) of
    25.6      ([], _) => (Path [Basic s], "")
    25.7 -  | (cs, e) => (Path [Basic (implode (Library.take (length cs - 1, cs)))], implode e)));
    25.8 +  | (cs, e) => (Path [Basic (implode ((uncurry take) (length cs - 1, cs)))], implode e)));
    25.9  
   25.10  
   25.11  (* expand variables *)
    26.1 --- a/src/Pure/General/scan.ML	Tue Nov 24 14:37:23 2009 +0100
    26.2 +++ b/src/Pure/General/scan.ML	Tue Nov 24 17:28:25 2009 +0100
    26.3 @@ -221,7 +221,7 @@
    26.4  
    26.5  fun trace scan xs =
    26.6    let val (y, xs') = scan xs
    26.7 -  in ((y, Library.take (length xs - length xs', xs)), xs') end;
    26.8 +  in ((y, (uncurry take) (length xs - length xs', xs)), xs') end;
    26.9  
   26.10  
   26.11  (* stopper *)
    27.1 --- a/src/Pure/General/symbol.ML	Tue Nov 24 14:37:23 2009 +0100
    27.2 +++ b/src/Pure/General/symbol.ML	Tue Nov 24 17:28:25 2009 +0100
    27.3 @@ -183,7 +183,7 @@
    27.4          val raw1 = raw0 o implode;
    27.5          val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
    27.6      
    27.7 -        fun encode cs = enc (Library.take_prefix raw_chr cs)
    27.8 +        fun encode cs = enc (take_prefix raw_chr cs)
    27.9          and enc ([], []) = []
   27.10            | enc (cs, []) = [raw1 cs]
   27.11            | enc ([], d :: ds) = raw2 d :: encode ds
   27.12 @@ -198,11 +198,11 @@
   27.13  
   27.14  fun beginning n cs =
   27.15    let
   27.16 -    val drop_blanks = #1 o Library.take_suffix is_ascii_blank;
   27.17 +    val drop_blanks = #1 o take_suffix is_ascii_blank;
   27.18      val all_cs = drop_blanks cs;
   27.19      val dots = if length all_cs > n then " ..." else "";
   27.20    in
   27.21 -    (drop_blanks (Library.take (n, all_cs))
   27.22 +    (drop_blanks (take n all_cs)
   27.23        |> map (fn c => if is_ascii_blank c then space else c)
   27.24        |> implode) ^ dots
   27.25    end;
   27.26 @@ -491,8 +491,8 @@
   27.27  
   27.28  fun strip_blanks s =
   27.29    sym_explode s
   27.30 -  |> Library.take_prefix is_blank |> #2
   27.31 -  |> Library.take_suffix is_blank |> #1
   27.32 +  |> take_prefix is_blank |> #2
   27.33 +  |> take_suffix is_blank |> #1
   27.34    |> implode;
   27.35  
   27.36  
   27.37 @@ -516,7 +516,7 @@
   27.38            then chr (ord s + 1) :: ss
   27.39            else "a" :: s :: ss;
   27.40  
   27.41 -    val (ss, qs) = apfst rev (Library.take_suffix is_quasi (sym_explode str));
   27.42 +    val (ss, qs) = apfst rev (take_suffix is_quasi (sym_explode str));
   27.43      val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   27.44    in implode (rev ss' @ qs) end;
   27.45  
    28.1 --- a/src/Pure/Isar/code.ML	Tue Nov 24 14:37:23 2009 +0100
    28.2 +++ b/src/Pure/Isar/code.ML	Tue Nov 24 17:28:25 2009 +0100
    28.3 @@ -128,7 +128,7 @@
    28.4      val args = args_of thm;
    28.5      val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
    28.6      fun matches_args args' = length args <= length args' andalso
    28.7 -      Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args');
    28.8 +      Pattern.matchess thy (args, (map incr_idx o curry (uncurry take) (length args)) args');
    28.9      fun drop (thm', proper') = if (proper orelse not proper')
   28.10        andalso matches_args (args_of thm') then 
   28.11          (warning ("Code generator: dropping redundant code equation\n" ^
    29.1 --- a/src/Pure/Isar/obtain.ML	Tue Nov 24 14:37:23 2009 +0100
    29.2 +++ b/src/Pure/Isar/obtain.ML	Tue Nov 24 17:28:25 2009 +0100
    29.3 @@ -232,12 +232,12 @@
    29.4          err ("Failed to unify variable " ^
    29.5            string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
    29.6            string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
    29.7 -    val (tyenv, _) = fold unify (map #1 vars ~~ Library.take (m, params))
    29.8 +    val (tyenv, _) = fold unify (map #1 vars ~~ (uncurry take) (m, params))
    29.9        (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
   29.10      val norm_type = Envir.norm_type tyenv;
   29.11  
   29.12      val xs = map (apsnd norm_type o fst) vars;
   29.13 -    val ys = map (apsnd norm_type) (Library.drop (m, params));
   29.14 +    val ys = map (apsnd norm_type) ((uncurry drop) (m, params));
   29.15      val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
   29.16      val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
   29.17  
    30.1 --- a/src/Pure/Isar/proof_context.ML	Tue Nov 24 14:37:23 2009 +0100
    30.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Nov 24 17:28:25 2009 +0100
    30.3 @@ -1340,7 +1340,7 @@
    30.4        val suppressed = len - ! prems_limit;
    30.5        val prt_prems = if null prems then []
    30.6          else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
    30.7 -          map (Display.pretty_thm ctxt) (Library.drop (suppressed, prems)))];
    30.8 +          map (Display.pretty_thm ctxt) ((uncurry drop) (suppressed, prems)))];
    30.9      in prt_structs @ prt_fixes @ prt_prems end;
   30.10  
   30.11  
    31.1 --- a/src/Pure/Isar/rule_cases.ML	Tue Nov 24 14:37:23 2009 +0100
    31.2 +++ b/src/Pure/Isar/rule_cases.ML	Tue Nov 24 17:28:25 2009 +0100
    31.3 @@ -144,7 +144,7 @@
    31.4            (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
    31.5          NONE => (name, NONE)
    31.6        | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
    31.7 -  in fold_rev add_case (Library.drop (n - nprems, cases)) ([], n) |> #1 end;
    31.8 +  in fold_rev add_case ((uncurry drop) (n - nprems, cases)) ([], n) |> #1 end;
    31.9  
   31.10  in
   31.11  
   31.12 @@ -205,8 +205,8 @@
   31.13      th
   31.14      |> unfold_prems n defs
   31.15      |> unfold_prems_concls defs
   31.16 -    |> Drule.multi_resolve (Library.take (m, facts))
   31.17 -    |> Seq.map (pair (xx, (n - m, Library.drop (m, facts))))
   31.18 +    |> Drule.multi_resolve ((uncurry take) (m, facts))
   31.19 +    |> Seq.map (pair (xx, (n - m, (uncurry drop) (m, facts))))
   31.20    end;
   31.21  
   31.22  end;
   31.23 @@ -345,7 +345,7 @@
   31.24  fun prep_rule n th =
   31.25    let
   31.26      val th' = Thm.permute_prems 0 n th;
   31.27 -    val prems = Library.take (Thm.nprems_of th' - n, Drule.cprems_of th');
   31.28 +    val prems = (uncurry take) (Thm.nprems_of th' - n, Drule.cprems_of th');
   31.29      val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
   31.30    in (prems, (n, th'')) end;
   31.31  
    32.1 --- a/src/Pure/Proof/extraction.ML	Tue Nov 24 14:37:23 2009 +0100
    32.2 +++ b/src/Pure/Proof/extraction.ML	Tue Nov 24 17:28:25 2009 +0100
    32.3 @@ -461,7 +461,7 @@
    32.4              end
    32.5            else (vs', tye)
    32.6  
    32.7 -      in fold_rev add_args (Library.take (n, vars) ~~ Library.take (n, ts)) ([], []) end;
    32.8 +      in fold_rev add_args ((uncurry take) (n, vars) ~~ (uncurry take) (n, ts)) ([], []) end;
    32.9  
   32.10      fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
   32.11      fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
    33.1 --- a/src/Pure/Syntax/ast.ML	Tue Nov 24 14:37:23 2009 +0100
    33.2 +++ b/src/Pure/Syntax/ast.ML	Tue Nov 24 17:28:25 2009 +0100
    33.3 @@ -158,7 +158,7 @@
    33.4        (case (ast, pat) of
    33.5          (Appl asts, Appl pats) =>
    33.6            let val a = length asts and p = length pats in
    33.7 -            if a > p then (Appl (Library.take (p, asts)), Library.drop (p, asts))
    33.8 +            if a > p then (Appl ((uncurry take) (p, asts)), (uncurry drop) (p, asts))
    33.9              else (ast, [])
   33.10            end
   33.11        | _ => (ast, []));
    34.1 --- a/src/Pure/Syntax/syntax.ML	Tue Nov 24 14:37:23 2009 +0100
    34.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Nov 24 17:28:25 2009 +0100
    34.3 @@ -499,7 +499,7 @@
    34.4          (("Ambiguous input" ^ Position.str_of pos ^
    34.5            "\nproduces " ^ string_of_int len ^ " parse trees" ^
    34.6            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
    34.7 -          map show_pt (Library.take (limit, pts)))));
    34.8 +          map show_pt ((uncurry take) (limit, pts)))));
    34.9      SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
   34.10    end;
   34.11  
   34.12 @@ -545,7 +545,7 @@
   34.13          else cat_error (ambig_msg ()) (cat_lines
   34.14            (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
   34.15              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   34.16 -            map (Pretty.string_of_term pp) (Library.take (limit, results))))
   34.17 +            map (Pretty.string_of_term pp) ((uncurry take) (limit, results))))
   34.18        end;
   34.19  
   34.20  fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
    35.1 --- a/src/Pure/Thy/present.ML	Tue Nov 24 14:37:23 2009 +0100
    35.2 +++ b/src/Pure/Thy/present.ML	Tue Nov 24 17:28:25 2009 +0100
    35.3 @@ -285,7 +285,7 @@
    35.4      (browser_info := empty_browser_info; session_info := NONE)
    35.5    else
    35.6      let
    35.7 -      val parent_name = name_of_session (Library.take (length path - 1, path));
    35.8 +      val parent_name = name_of_session ((uncurry take) (length path - 1, path));
    35.9        val session_name = name_of_session path;
   35.10        val sess_prefix = Path.make path;
   35.11        val html_prefix = Path.append (Path.expand output_path) sess_prefix;
    36.1 --- a/src/Pure/Thy/thy_output.ML	Tue Nov 24 14:37:23 2009 +0100
    36.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Nov 24 17:28:25 2009 +0100
    36.3 @@ -265,7 +265,7 @@
    36.4        if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
    36.5        else if nesting >= 0 then (tag', replicate nesting tag @ tags)
    36.6        else
    36.7 -        (case Library.drop (~ nesting - 1, tags) of
    36.8 +        (case (uncurry drop) (~ nesting - 1, tags) of
    36.9            tgs :: tgss => (tgs, tgss)
   36.10          | [] => err_bad_nesting (Position.str_of cmd_pos));
   36.11  
    37.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Nov 24 14:37:23 2009 +0100
    37.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Nov 24 17:28:25 2009 +0100
    37.3 @@ -409,7 +409,7 @@
    37.4  
    37.5          val len = length matches;
    37.6          val lim = the_default (! limit) opt_limit;
    37.7 -      in (SOME len, Library.drop (len - lim, matches)) end;
    37.8 +      in (SOME len, (uncurry drop) (len - lim, matches)) end;
    37.9  
   37.10      val find =
   37.11        if rem_dups orelse is_none opt_limit
    38.1 --- a/src/Pure/assumption.ML	Tue Nov 24 14:37:23 2009 +0100
    38.2 +++ b/src/Pure/assumption.ML	Tue Nov 24 17:28:25 2009 +0100
    38.3 @@ -88,12 +88,12 @@
    38.4  (* local assumptions *)
    38.5  
    38.6  fun local_assumptions_of inner outer =
    38.7 -  Library.drop (length (all_assumptions_of outer), all_assumptions_of inner);
    38.8 +  (uncurry drop) (length (all_assumptions_of outer), all_assumptions_of inner);
    38.9  
   38.10  val local_assms_of = maps #2 oo local_assumptions_of;
   38.11  
   38.12  fun local_prems_of inner outer =
   38.13 -  Library.drop (length (all_prems_of outer), all_prems_of inner);
   38.14 +  (uncurry drop) (length (all_prems_of outer), all_prems_of inner);
   38.15  
   38.16  
   38.17  (* add assumptions *)
    39.1 --- a/src/Pure/codegen.ML	Tue Nov 24 14:37:23 2009 +0100
    39.2 +++ b/src/Pure/codegen.ML	Tue Nov 24 17:28:25 2009 +0100
    39.3 @@ -579,11 +579,11 @@
    39.4  fun eta_expand t ts i =
    39.5    let
    39.6      val k = length ts;
    39.7 -    val Ts = Library.drop (k, binder_types (fastype_of t));
    39.8 +    val Ts = (uncurry drop) (k, binder_types (fastype_of t));
    39.9      val j = i - k
   39.10    in
   39.11      List.foldr (fn (T, t) => Abs ("x", T, t))
   39.12 -      (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
   39.13 +      (list_comb (t, ts @ map Bound (j-1 downto 0))) ((uncurry take) (j, Ts))
   39.14    end;
   39.15  
   39.16  fun mk_app _ p [] = p
    40.1 --- a/src/Pure/goal_display.ML	Tue Nov 24 14:37:23 2009 +0100
    40.2 +++ b/src/Pure/goal_display.ML	Tue Nov 24 17:28:25 2009 +0100
    40.3 @@ -99,7 +99,7 @@
    40.4        (if main then [prt_term B] else []) @
    40.5         (if ngoals = 0 then [Pretty.str "No subgoals!"]
    40.6          else if ngoals > maxgoals then
    40.7 -          pretty_subgoals (Library.take (maxgoals, As)) @
    40.8 +          pretty_subgoals ((uncurry take) (maxgoals, As)) @
    40.9            (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   40.10             else [])
   40.11          else pretty_subgoals As) @
    41.1 --- a/src/Pure/library.ML	Tue Nov 24 14:37:23 2009 +0100
    41.2 +++ b/src/Pure/library.ML	Tue Nov 24 17:28:25 2009 +0100
    41.3 @@ -81,6 +81,8 @@
    41.4    val filter: ('a -> bool) -> 'a list -> 'a list
    41.5    val filter_out: ('a -> bool) -> 'a list -> 'a list
    41.6    val map_filter: ('a -> 'b option) -> 'a list -> 'b list
    41.7 +  val take: int -> 'a list -> 'a list
    41.8 +  val drop: int -> 'a list -> 'a list
    41.9    val chop: int -> 'a list -> 'a list * 'a list
   41.10    val dropwhile: ('a -> bool) -> 'a list -> 'a list
   41.11    val nth: 'a list -> int -> 'a
   41.12 @@ -224,8 +226,6 @@
   41.13    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
   41.14    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   41.15    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   41.16 -  val take: int * 'a list -> 'a list
   41.17 -  val drop: int * 'a list -> 'a list
   41.18    val last_elem: 'a list -> 'a
   41.19  end;
   41.20  
   41.21 @@ -423,20 +423,20 @@
   41.22  fun filter_out f = filter (not o f);
   41.23  val map_filter = List.mapPartial;
   41.24  
   41.25 +fun take (0: int) xs = []
   41.26 +  | take _ [] = []
   41.27 +  | take n (x :: xs) =
   41.28 +      if n > 0 then x :: take (n - 1) xs else [];
   41.29 +
   41.30 +fun drop (0: int) xs = xs
   41.31 +  | drop _ [] = []
   41.32 +  | drop n (x :: xs) =
   41.33 +      if n > 0 then drop (n - 1) xs else x :: xs;
   41.34 +
   41.35  fun chop (0: int) xs = ([], xs)
   41.36    | chop _ [] = ([], [])
   41.37    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
   41.38  
   41.39 -(*take the first n elements from a list*)
   41.40 -fun take (n: int, []) = []
   41.41 -  | take (n, x :: xs) =
   41.42 -      if n > 0 then x :: take (n - 1, xs) else [];
   41.43 -
   41.44 -(*drop the first n elements from a list*)
   41.45 -fun drop (n: int, []) = []
   41.46 -  | drop (n, x :: xs) =
   41.47 -      if n > 0 then drop (n - 1, xs) else x :: xs;
   41.48 -
   41.49  fun dropwhile P [] = []
   41.50    | dropwhile P (ys as x::xs) = if P x then dropwhile P xs else ys;
   41.51  
    42.1 --- a/src/Pure/meta_simplifier.ML	Tue Nov 24 14:37:23 2009 +0100
    42.2 +++ b/src/Pure/meta_simplifier.ML	Tue Nov 24 17:28:25 2009 +0100
    42.3 @@ -1163,9 +1163,9 @@
    42.4                val (rrs', asm') = rules_of_prem ss prem'
    42.5              in mut_impc prems concl rrss asms (prem' :: prems')
    42.6                (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
    42.7 -                (Library.take (i, prems))
    42.8 +                ((uncurry take) (i, prems))
    42.9                  (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
   42.10 -                  (Library.drop (i, prems), concl))))) :: eqns)
   42.11 +                  ((uncurry drop) (i, prems), concl))))) :: eqns)
   42.12                    ss (length prems') ~1
   42.13              end
   42.14  
    43.1 --- a/src/Pure/proofterm.ML	Tue Nov 24 14:37:23 2009 +0100
    43.2 +++ b/src/Pure/proofterm.ML	Tue Nov 24 17:28:25 2009 +0100
    43.3 @@ -1003,7 +1003,7 @@
    43.4                | _ => error "shrink: proof not in normal form");
    43.5              val vs = vars_of prop;
    43.6              val (ts', ts'') = chop (length vs) ts;
    43.7 -            val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts';
    43.8 +            val insts = (uncurry take) (length ts', map (fst o dest_Var) vs) ~~ ts';
    43.9              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
   43.10                insert (op =) ixn (case AList.lookup (op =) insts ixn of
   43.11                    SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
    44.1 --- a/src/Pure/tactic.ML	Tue Nov 24 14:37:23 2009 +0100
    44.2 +++ b/src/Pure/tactic.ML	Tue Nov 24 17:28:25 2009 +0100
    44.3 @@ -173,7 +173,7 @@
    44.4    perm_tac 0 (1 - i);
    44.5  
    44.6  fun distinct_subgoal_tac i st =
    44.7 -  (case Library.drop (i - 1, Thm.prems_of st) of
    44.8 +  (case (uncurry drop) (i - 1, Thm.prems_of st) of
    44.9      [] => no_tac st
   44.10    | A :: Bs =>
   44.11        st |> EVERY (fold (fn (B, k) =>
    45.1 --- a/src/Pure/thm.ML	Tue Nov 24 14:37:23 2009 +0100
    45.2 +++ b/src/Pure/thm.ML	Tue Nov 24 17:28:25 2009 +0100
    45.3 @@ -1457,7 +1457,7 @@
    45.4      val short = length iparams - length cs;
    45.5      val newnames =
    45.6        if short < 0 then error "More names than abstractions!"
    45.7 -      else Name.variant_list cs (Library.take (short, iparams)) @ cs;
    45.8 +      else Name.variant_list cs ((uncurry take) (short, iparams)) @ cs;
    45.9      val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
   45.10      val newBi = Logic.list_rename_params (newnames, Bi);
   45.11    in
    46.1 --- a/src/Pure/variable.ML	Tue Nov 24 14:37:23 2009 +0100
    46.2 +++ b/src/Pure/variable.ML	Tue Nov 24 17:28:25 2009 +0100
    46.3 @@ -345,7 +345,7 @@
    46.4      val fixes_inner = fixes_of inner;
    46.5      val fixes_outer = fixes_of outer;
    46.6  
    46.7 -    val gen_fixes = map #2 (Library.take (length fixes_inner - length fixes_outer, fixes_inner));
    46.8 +    val gen_fixes = map #2 ((uncurry take) (length fixes_inner - length fixes_outer, fixes_inner));
    46.9      val still_fixed = not o member (op =) gen_fixes;
   46.10  
   46.11      val type_occs_inner = type_occs_of inner;
    47.1 --- a/src/Tools/Code/code_haskell.ML	Tue Nov 24 14:37:23 2009 +0100
    47.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Nov 24 17:28:25 2009 +0100
    47.3 @@ -78,7 +78,7 @@
    47.4      and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    47.5       of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
    47.6        | fingerprint => let
    47.7 -          val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
    47.8 +          val ts_fingerprint = ts ~~ curry (uncurry take) (length ts) fingerprint;
    47.9            val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
   47.10              (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
   47.11            fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t
   47.12 @@ -86,7 +86,7 @@
   47.13                  brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty];
   47.14          in
   47.15            if needs_annotation then
   47.16 -            (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
   47.17 +            (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry (uncurry take) (length ts) tys)
   47.18            else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
   47.19          end
   47.20      and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
    48.1 --- a/src/Tools/Code/code_printer.ML	Tue Nov 24 14:37:23 2009 +0100
    48.2 +++ b/src/Tools/Code/code_printer.ML	Tue Nov 24 17:28:25 2009 +0100
    48.3 @@ -231,7 +231,7 @@
    48.4     of NONE => brackify fxy (pr_app thm vars app)
    48.5      | SOME (k, pr) =>
    48.6          let
    48.7 -          fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry Library.take k tys);
    48.8 +          fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry (uncurry take) k tys);
    48.9          in if k = length ts
   48.10            then pr' fxy ts
   48.11          else if k < length ts
    49.1 --- a/src/Tools/Code/code_thingol.ML	Tue Nov 24 14:37:23 2009 +0100
    49.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Nov 24 17:28:25 2009 +0100
    49.3 @@ -226,7 +226,7 @@
    49.4      val l = k - j;
    49.5      val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
    49.6      val vs_tys = (map o apfst) SOME
    49.7 -      (Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys));
    49.8 +      (Name.names ctxt "a" ((curry (uncurry take) l o curry (uncurry drop) j) tys));
    49.9    in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
   49.10  
   49.11  fun contains_dictvar t =
   49.12 @@ -773,7 +773,7 @@
   49.13          val clauses = if null case_pats
   49.14            then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
   49.15            else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
   49.16 -            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry Library.take n tys) t)
   49.17 +            mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry (uncurry take) n tys) t)
   49.18                (constrs ~~ ts_clause);
   49.19        in ((t, ty), clauses) end;
   49.20    in
   49.21 @@ -788,7 +788,7 @@
   49.22    if length ts < num_args then
   49.23      let
   49.24        val k = length ts;
   49.25 -      val tys = (curry Library.take (num_args - k) o curry Library.drop k o fst o strip_type) ty;
   49.26 +      val tys = (curry (uncurry take) (num_args - k) o curry (uncurry drop) k o fst o strip_type) ty;
   49.27        val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
   49.28        val vs = Name.names ctxt "a" tys;
   49.29      in
   49.30 @@ -797,8 +797,8 @@
   49.31        #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
   49.32      end
   49.33    else if length ts > num_args then
   49.34 -    translate_case thy algbr eqngr thm case_scheme ((c, ty), Library.take (num_args, ts))
   49.35 -    ##>> fold_map (translate_term thy algbr eqngr thm) (Library.drop (num_args, ts))
   49.36 +    translate_case thy algbr eqngr thm case_scheme ((c, ty), (uncurry take) (num_args, ts))
   49.37 +    ##>> fold_map (translate_term thy algbr eqngr thm) ((uncurry drop) (num_args, ts))
   49.38      #>> (fn (t, ts) => t `$$ ts)
   49.39    else
   49.40      translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
    50.1 --- a/src/Tools/induct.ML	Tue Nov 24 14:37:23 2009 +0100
    50.2 +++ b/src/Tools/induct.ML	Tue Nov 24 17:28:25 2009 +0100
    50.3 @@ -280,11 +280,11 @@
    50.4  
    50.5  fun align_left msg xs ys =
    50.6    let val m = length xs and n = length ys
    50.7 -  in if m < n then error msg else (Library.take (n, xs) ~~ ys) end;
    50.8 +  in if m < n then error msg else ((uncurry take) (n, xs) ~~ ys) end;
    50.9  
   50.10  fun align_right msg xs ys =
   50.11    let val m = length xs and n = length ys
   50.12 -  in if m < n then error msg else (Library.drop (m - n, xs) ~~ ys) end;
   50.13 +  in if m < n then error msg else ((uncurry drop) (m - n, xs) ~~ ys) end;
   50.14  
   50.15  
   50.16  (* prep_inst *)
    51.1 --- a/src/Tools/induct_tacs.ML	Tue Nov 24 14:37:23 2009 +0100
    51.2 +++ b/src/Tools/induct_tacs.ML	Tue Nov 24 17:28:25 2009 +0100
    51.3 @@ -59,7 +59,7 @@
    51.4  
    51.5  fun prep_inst (concl, xs) =
    51.6    let val vs = Induct.vars_of concl
    51.7 -  in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end;
    51.8 +  in map_filter prep_var ((uncurry drop) (length vs - length xs, vs) ~~ xs) end;
    51.9  
   51.10  in
   51.11  
    52.1 --- a/src/ZF/Tools/cartprod.ML	Tue Nov 24 14:37:23 2009 +0100
    52.2 +++ b/src/ZF/Tools/cartprod.ML	Tue Nov 24 17:28:25 2009 +0100
    52.3 @@ -97,7 +97,7 @@
    52.4  (*Makes a nested tuple from a list, following the product type structure*)
    52.5  fun mk_tuple pair (Type("*", [T1,T2])) tms = 
    52.6          pair $ (mk_tuple pair T1 tms)
    52.7 -             $ (mk_tuple pair T2 (Library.drop (length (factors T1), tms)))
    52.8 +             $ (mk_tuple pair T2 ((uncurry drop) (length (factors T1), tms)))
    52.9    | mk_tuple pair T (t::_) = t;
   52.10  
   52.11  (*Attempts to remove occurrences of split, and pair-valued parameters*)