--- a/src/HOL/Nominal/nominal_datatype.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Nov 25 09:13:46 2009 +0100
@@ -766,8 +766,8 @@
Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
val recTs = get_rec_types descr'' sorts;
- val newTs' = (uncurry take) (length new_type_names, recTs');
- val newTs = (uncurry take) (length new_type_names, recTs);
+ val newTs' = take (length new_type_names) recTs';
+ val newTs = take (length new_type_names) recTs;
val full_new_type_names = map (Sign.full_bname thy) new_type_names;
--- a/src/HOL/Nominal/nominal_induct.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Wed Nov 25 09:13:46 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 = (uncurry drop) (m - n - 2, ys);
+ val zs = 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) ((uncurry take) (p - n, ps)) @ xs;
+ else map (tune o #1) (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)
--- a/src/HOL/Tools/Datatype/datatype.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Wed Nov 25 09:13:46 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 ""]))
- ((uncurry drop) (length dt_names, inducts));
+ (drop (length dt_names) inducts);
in
thy9
|> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Nov 25 09:13:46 2009 +0100
@@ -51,7 +51,7 @@
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
- val newTs = (uncurry take) (length (hd descr), recTs);
+ val newTs = 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 = (uncurry take) (i, dummyPs) @ (P::((uncurry drop) (i + 1, dummyPs)));
+ val insts = take i dummyPs @ (P::(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 = (uncurry take) (length (hd descr), recTs);
+ val newTs = 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 = (uncurry take) (length (hd descr), recTs);
+ val newTs = 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';
@@ -305,8 +305,8 @@
let
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 = (uncurry take) (length cargs, frees');
+ val frees' = map2 (mk_Free "x") Ts' (1 upto length Ts');
+ val frees = 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 ((uncurry take) (i, case_dummy_fns)) @
- fns2 @ flat ((uncurry drop) (i + 1, case_dummy_fns));
+ val fns = flat (take i case_dummy_fns) @
+ fns2 @ flat (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 ((uncurry take) (i, case_dummy_fns))) @
- fns2 @ (flat ((uncurry drop) (i + 1, case_dummy_fns))) )));
+ list_comb (reccomb, (flat (take i case_dummy_fns)) @
+ fns2 @ (flat (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 ~~
- (uncurry take) (length newTs, reccomb_names)) ([], thy1)
+ 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 = (uncurry take) (length (hd descr), recTs);
+ val newTs = take (length (hd descr)) recTs;
fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
exhaustion), case_thms'), T) =
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Nov 25 09:13:46 2009 +0100
@@ -217,19 +217,19 @@
invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
else
let
- val ts1 = (uncurry take) (i, ts);
- val t :: ts2 = (uncurry drop) (i, ts);
+ val ts1 = take i ts;
+ val t :: ts2 = 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 ((uncurry take) (i+1, fst (strip_type T)));
+ val (Ts, dT) = split_last (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' = (uncurry take) (j, fst (strip_type U));
- val frees = map Free (xs ~~ Us');
+ val Us' = take j (fst (strip_type U));
+ val frees = map2 (curry Free) xs Us';
val (cp, gr0) = invoke_codegen thy defs dep module false
(list_comb (Const (cname, Us' ---> dT), frees)) gr;
val t' = Envir.beta_norm (list_comb (t, frees));
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Nov 25 09:13:46 2009 +0100
@@ -72,7 +72,7 @@
end;
in
map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
- (hd descr) ((uncurry take) (length (hd descr), get_rec_types descr' sorts))
+ (hd descr) (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 = (uncurry take) (length (hd descr), recTs);
+ val newTs = take (length (hd descr)) recTs;
fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
@@ -168,14 +168,12 @@
HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
end;
- fun make_casedist ((_, (_, _, constrs)), T) =
+ fun make_casedist ((_, (_, _, constrs))) T =
let val prems = map (make_casedist_prem T) constrs
in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))
end
- in map make_casedist
- ((hd descr) ~~ (uncurry take) (length (hd descr), get_rec_types descr' sorts))
- end;
+ in map2 make_casedist (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts)) end;
(*************** characteristic equations for primrec combinator **************)
@@ -257,7 +255,7 @@
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
- val newTs = (uncurry take) (length (hd descr), recTs);
+ val newTs = take (length (hd descr)) recTs;
val T' = TFree (Name.variant used "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
@@ -280,7 +278,7 @@
let
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
- val newTs = (uncurry take) (length (hd descr), recTs);
+ val newTs = take (length (hd descr)) recTs;
fun make_case T comb_t ((cname, cargs), f) =
let
@@ -304,7 +302,7 @@
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
- val newTs = (uncurry take) (length (hd descr), recTs);
+ val newTs = take (length (hd descr)) recTs;
val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
@@ -415,7 +413,7 @@
let
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
- val newTs = (uncurry take) (length (hd descr), recTs);
+ val newTs = take (length (hd descr)) recTs;
fun mk_eqn T (cname, cargs) =
let
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Nov 25 09:13:46 2009 +0100
@@ -77,8 +77,7 @@
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 = (uncurry take) (length (hd descr), recTs);
- val oldTs = (uncurry drop) (length (hd descr), recTs);
+ val (newTs, oldTs) = chop (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 +192,7 @@
QUIET_BREADTH_FIRST (has_fewer_prems 1)
(resolve_tac rep_intrs 1)))
(types_syntax ~~ tyvars ~~
- ((uncurry take) (length newTs, rep_set_names)) ~~ new_type_names) ||>
+ (take (length newTs) rep_set_names) ~~ new_type_names) ||>
Sign.add_path big_name;
(*********************** definition of constructors ***********************)
@@ -472,7 +471,7 @@
iso_inj_thms_unfolded;
val iso_thms = if length descr = 1 then [] else
- (uncurry drop) (length newTs, split_conj_thm
+ 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),
--- a/src/HOL/Tools/Function/fun.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML Wed Nov 25 09:13:46 2009 +0100
@@ -121,9 +121,9 @@
(Function_Split.split_all_equations ctxt compleqs)
fun restore_spec thms =
- bnds ~~ (uncurry take) (length bnds, Library.unflat spliteqs thms)
+ bnds ~~ take (length bnds) (unflat spliteqs thms)
- val spliteqs' = flat ((uncurry take) (length bnds, spliteqs))
+ val spliteqs' = flat (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'
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Nov 25 09:13:46 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,(uncurry take) (length qs, rs) ~~ vars)
+ in (eq, take (length qs) rs ~~ vars)
end;
fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
in
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Nov 25 09:13:46 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 = (uncurry take) (max_scopes, all)
+ val head = take max_scopes all
val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
head
in
--- a/src/HOL/Tools/inductive.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Nov 25 09:13:46 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 = (uncurry drop) (k, binder_types (fastype_of c));
+fun arg_types_of k c = drop k (binder_types (fastype_of c));
fun find_arg T x [] = sys_error "find_arg"
| find_arg T x ((p as (_, (SOME _, _))) :: ps) =
--- a/src/HOL/Tools/inductive_realizer.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Nov 25 09:13:46 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 ((uncurry take) (nparms, ts));
+ val params = map dest_Var (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) []))) @
--- a/src/HOL/Tools/old_primrec.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML Wed Nov 25 09:13:46 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 = (uncurry take) (rpos, ts);
- val rest = (uncurry drop) (rpos, ts);
+ val ls = take rpos ts;
+ val rest = 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");
--- a/src/HOL/Tools/record.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/record.ML Wed Nov 25 09:13:46 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 (uncurry take) (i, rTs);
+ val rTs' = if i < 0 then rTs else 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 ((uncurry drop) (length params, ys)) of
+ (case rev (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 = (uncurry take) (16, xs) :: group16 ((uncurry drop) (16, xs));
+ | group16 xs = take 16 xs :: group16 (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 = (uncurry take) (l, xs) :: chunks ls ((uncurry drop) (l, xs));
+ | chunks (l :: ls) xs = take l xs :: chunks ls (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 ((uncurry drop) (n, parents))) extT;
+ fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
val rec_schemeT0 = rec_schemeT 0;
fun recT n =
let val (c, Ts) = extension in
- mk_recordT (map #extension ((uncurry drop) (n, parents)))
+ mk_recordT (map #extension (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' ((uncurry drop) (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
+ fold_rev mk_ext' (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 = (uncurry drop) (parent_fields_len, xs);
+ fun lastN xs = drop parent_fields_len xs;
(*selectors*)
fun mk_sel_spec ((c, T), thm) =
--- a/src/HOL/Tools/split_rule.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML Wed Nov 25 09:13:46 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 = (uncurry take) (length ts, Us');
- val U = (uncurry drop) (length ts, Us') ---> U';
+ val Us = take (length ts) Us';
+ val U = drop (length ts) Us' ---> U';
val T' = maps HOLogic.flatten_tupleT Us ---> U;
fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
let
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Nov 25 09:13:46 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 = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
+ fun strip ss = 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 = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
+ fun strip ss = 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
--- a/src/Pure/General/path.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/General/path.ML Wed Nov 25 09:13:46 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 ((uncurry take) (length cs - 1, cs)))], implode e)));
+ | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
(* expand variables *)
--- a/src/Pure/General/scan.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/General/scan.ML Wed Nov 25 09:13:46 2009 +0100
@@ -221,7 +221,7 @@
fun trace scan xs =
let val (y, xs') = scan xs
- in ((y, (uncurry take) (length xs - length xs', xs)), xs') end;
+ in ((y, take (length xs - length xs') xs), xs') end;
(* stopper *)
--- a/src/Pure/Isar/code.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Isar/code.ML Wed Nov 25 09:13:46 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 (uncurry take) (length args)) args');
+ Pattern.matchess thy (args, (map incr_idx o 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" ^
--- a/src/Pure/Isar/obtain.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Isar/obtain.ML Wed Nov 25 09:13:46 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 ~~ (uncurry take) (m, params))
+ val (tyenv, _) = fold unify (map #1 vars ~~ 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) ((uncurry drop) (m, params));
+ val ys = map (apsnd norm_type) (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');
--- a/src/Pure/Isar/proof_context.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Nov 25 09:13:46 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) ((uncurry drop) (suppressed, prems)))];
+ map (Display.pretty_thm ctxt) (drop suppressed prems))];
in prt_structs @ prt_fixes @ prt_prems end;
--- a/src/Pure/Isar/rule_cases.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML Wed Nov 25 09:13:46 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 ((uncurry drop) (n - nprems, cases)) ([], n) |> #1 end;
+ in fold_rev add_case (drop (n - nprems) cases) ([], n) |> #1 end;
in
@@ -205,8 +205,8 @@
th
|> unfold_prems n defs
|> unfold_prems_concls defs
- |> Drule.multi_resolve ((uncurry take) (m, facts))
- |> Seq.map (pair (xx, (n - m, (uncurry drop) (m, facts))))
+ |> Drule.multi_resolve (take m facts)
+ |> Seq.map (pair (xx, (n - m, 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 = (uncurry take) (Thm.nprems_of th' - n, Drule.cprems_of th');
+ val prems = 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;
--- a/src/Pure/Proof/extraction.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Wed Nov 25 09:13:46 2009 +0100
@@ -461,7 +461,7 @@
end
else (vs', tye)
- in fold_rev add_args ((uncurry take) (n, vars) ~~ (uncurry take) (n, ts)) ([], []) end;
+ in fold_rev add_args (take n vars ~~ 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);
--- a/src/Pure/Syntax/ast.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Syntax/ast.ML Wed Nov 25 09:13:46 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 ((uncurry take) (p, asts)), (uncurry drop) (p, asts))
+ if a > p then (Appl (take p asts), drop p asts)
else (ast, [])
end
| _ => (ast, []));
--- a/src/Pure/Syntax/syntax.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Nov 25 09:13:46 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 ((uncurry take) (limit, pts)))));
+ map show_pt (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) ((uncurry take) (limit, results))))
+ map (Pretty.string_of_term pp) (take limit results)))
end;
fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
--- a/src/Pure/Thy/present.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Thy/present.ML Wed Nov 25 09:13:46 2009 +0100
@@ -285,7 +285,7 @@
(browser_info := empty_browser_info; session_info := NONE)
else
let
- val parent_name = name_of_session ((uncurry take) (length path - 1, path));
+ val parent_name = name_of_session (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;
--- a/src/Pure/Thy/thy_output.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Nov 25 09:13:46 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 (uncurry drop) (~ nesting - 1, tags) of
+ (case drop (~ nesting - 1) tags of
tgs :: tgss => (tgs, tgss)
| [] => err_bad_nesting (Position.str_of cmd_pos));
--- a/src/Pure/Tools/find_theorems.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Wed Nov 25 09:13:46 2009 +0100
@@ -409,7 +409,7 @@
val len = length matches;
val lim = the_default (! limit) opt_limit;
- in (SOME len, (uncurry drop) (len - lim, matches)) end;
+ in (SOME len, drop (len - lim) matches) end;
val find =
if rem_dups orelse is_none opt_limit
--- a/src/Pure/assumption.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/assumption.ML Wed Nov 25 09:13:46 2009 +0100
@@ -88,12 +88,12 @@
(* local assumptions *)
fun local_assumptions_of inner outer =
- (uncurry drop) (length (all_assumptions_of outer), all_assumptions_of inner);
+ 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 =
- (uncurry drop) (length (all_prems_of outer), all_prems_of inner);
+ drop (length (all_prems_of outer)) (all_prems_of inner);
(* add assumptions *)
--- a/src/Pure/codegen.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/codegen.ML Wed Nov 25 09:13:46 2009 +0100
@@ -579,11 +579,11 @@
fun eta_expand t ts i =
let
val k = length ts;
- val Ts = (uncurry drop) (k, binder_types (fastype_of t));
+ val Ts = 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))) ((uncurry take) (j, Ts))
+ (list_comb (t, ts @ map Bound (j-1 downto 0))) (take j Ts)
end;
fun mk_app _ p [] = p
--- a/src/Pure/goal_display.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/goal_display.ML Wed Nov 25 09:13:46 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 ((uncurry take) (maxgoals, As)) @
+ pretty_subgoals (take maxgoals As) @
(if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
else [])
else pretty_subgoals As) @
--- a/src/Pure/meta_simplifier.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/meta_simplifier.ML Wed Nov 25 09:13:46 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)
- ((uncurry take) (i, prems))
+ (take i prems)
(Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
- ((uncurry drop) (i, prems), concl))))) :: eqns)
+ (drop i prems, concl))))) :: eqns)
ss (length prems') ~1
end
--- a/src/Pure/proofterm.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/proofterm.ML Wed Nov 25 09:13:46 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 = (uncurry take) (length ts', map (fst o dest_Var) vs) ~~ ts';
+ val insts = 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'
--- a/src/Pure/tactic.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/tactic.ML Wed Nov 25 09:13:46 2009 +0100
@@ -173,7 +173,7 @@
perm_tac 0 (1 - i);
fun distinct_subgoal_tac i st =
- (case (uncurry drop) (i - 1, Thm.prems_of st) of
+ (case drop (i - 1) (Thm.prems_of st) of
[] => no_tac st
| A :: Bs =>
st |> EVERY (fold (fn (B, k) =>
--- a/src/Pure/thm.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/thm.ML Wed Nov 25 09:13:46 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 ((uncurry take) (short, iparams)) @ cs;
+ else Name.variant_list cs (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
--- a/src/Pure/variable.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/variable.ML Wed Nov 25 09:13:46 2009 +0100
@@ -345,7 +345,7 @@
val fixes_inner = fixes_of inner;
val fixes_outer = fixes_of outer;
- val gen_fixes = map #2 ((uncurry take) (length fixes_inner - length fixes_outer, fixes_inner));
+ val gen_fixes = map #2 (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;
--- a/src/Tools/Code/code_haskell.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Tools/Code/code_haskell.ML Wed Nov 25 09:13:46 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 (uncurry take) (length ts) fingerprint;
+ val ts_fingerprint = ts ~~ 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 (uncurry take) (length ts) tys)
+ (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (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
--- a/src/Tools/Code/code_printer.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Tools/Code/code_printer.ML Wed Nov 25 09:13:46 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 (uncurry take) k tys);
+ fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ take k tys);
in if k = length ts
then pr' fxy ts
else if k < length ts
--- a/src/Tools/Code/code_thingol.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML Wed Nov 25 09:13:46 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 (uncurry take) l o curry (uncurry drop) j) tys));
+ (Name.names ctxt "a" ((take l o 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 (uncurry take) n tys) t)
+ mk_clause (fn (ts, body) => (constr `$$ ts, body)) (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 (uncurry take) (num_args - k) o curry (uncurry drop) k o fst o strip_type) ty;
+ val tys = (take (num_args - k) o 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), (uncurry take) (num_args, ts))
- ##>> fold_map (translate_term thy algbr eqngr thm) ((uncurry drop) (num_args, ts))
+ translate_case thy algbr eqngr thm case_scheme ((c, ty), take num_args ts)
+ ##>> fold_map (translate_term thy algbr eqngr thm) (drop num_args ts)
#>> (fn (t, ts) => t `$$ ts)
else
translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
--- a/src/Tools/induct.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Tools/induct.ML Wed Nov 25 09:13:46 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 ((uncurry take) (n, xs) ~~ ys) end;
+ in if m < n then error msg else (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 ((uncurry drop) (m - n, xs) ~~ ys) end;
+ in if m < n then error msg else (drop (m - n) xs ~~ ys) end;
(* prep_inst *)
--- a/src/Tools/induct_tacs.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Tools/induct_tacs.ML Wed Nov 25 09:13:46 2009 +0100
@@ -59,7 +59,7 @@
fun prep_inst (concl, xs) =
let val vs = Induct.vars_of concl
- in map_filter prep_var ((uncurry drop) (length vs - length xs, vs) ~~ xs) end;
+ in map_filter prep_var (drop (length vs - length xs) vs ~~ xs) end;
in
--- a/src/ZF/Tools/cartprod.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/ZF/Tools/cartprod.ML Wed Nov 25 09:13:46 2009 +0100
@@ -96,8 +96,8 @@
(*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 ((uncurry drop) (length (factors T1), tms)))
+ pair $ mk_tuple pair T1 tms
+ $ mk_tuple pair T2 (drop (length (factors T1)) tms)
| mk_tuple pair T (t::_) = t;
(*Attempts to remove occurrences of split, and pair-valued parameters*)