1.1 --- a/src/HOL/Nominal/nominal_datatype.ML Tue Nov 24 17:28:44 2009 +0100
1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Nov 25 09:13:46 2009 +0100
1.3 @@ -766,8 +766,8 @@
1.4 Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names;
1.5
1.6 val recTs = get_rec_types descr'' sorts;
1.7 - val newTs' = (uncurry take) (length new_type_names, recTs');
1.8 - val newTs = (uncurry take) (length new_type_names, recTs);
1.9 + val newTs' = take (length new_type_names) recTs';
1.10 + val newTs = take (length new_type_names) recTs;
1.11
1.12 val full_new_type_names = map (Sign.full_bname thy) new_type_names;
1.13
2.1 --- a/src/HOL/Nominal/nominal_induct.ML Tue Nov 24 17:28:44 2009 +0100
2.2 +++ b/src/HOL/Nominal/nominal_induct.ML Wed Nov 25 09:13:46 2009 +0100
2.3 @@ -46,7 +46,7 @@
2.4 val m = length vars and n = length inst;
2.5 val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule";
2.6 val P :: x :: ys = vars;
2.7 - val zs = (uncurry drop) (m - n - 2, ys);
2.8 + val zs = drop (m - n - 2) ys;
2.9 in
2.10 (P, tuple_fun (map #2 avoiding) (Term.dest_Var P)) ::
2.11 (x, tuple (map Free avoiding)) ::
2.12 @@ -71,7 +71,7 @@
2.13 val p = length ps;
2.14 val ys =
2.15 if p < n then []
2.16 - else map (tune o #1) ((uncurry take) (p - n, ps)) @ xs;
2.17 + else map (tune o #1) (take (p - n) ps) @ xs;
2.18 in Logic.list_rename_params (ys, prem) end;
2.19 fun rename_prems prop =
2.20 let val (As, C) = Logic.strip_horn (Thm.prop_of rule)
3.1 --- a/src/HOL/Tools/Datatype/datatype.ML Tue Nov 24 17:28:44 2009 +0100
3.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Nov 25 09:13:46 2009 +0100
3.3 @@ -328,7 +328,7 @@
3.4 ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
3.5 val unnamed_rules = map (fn induct =>
3.6 ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
3.7 - ((uncurry drop) (length dt_names, inducts));
3.8 + (drop (length dt_names) inducts);
3.9 in
3.10 thy9
3.11 |> PureThy.add_thmss ([((prfx (Binding.name "simps"), simps), []),
4.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Nov 24 17:28:44 2009 +0100
4.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Nov 25 09:13:46 2009 +0100
4.3 @@ -51,7 +51,7 @@
4.4
4.5 val descr' = flat descr;
4.6 val recTs = get_rec_types descr' sorts;
4.7 - val newTs = (uncurry take) (length (hd descr), recTs);
4.8 + val newTs = take (length (hd descr)) recTs;
4.9
4.10 val {maxidx, ...} = rep_thm induct;
4.11 val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
4.12 @@ -62,7 +62,7 @@
4.13 Abs ("z", T', Const ("True", T''))) induct_Ps;
4.14 val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
4.15 Var (("P", 0), HOLogic.boolT))
4.16 - val insts = (uncurry take) (i, dummyPs) @ (P::((uncurry drop) (i + 1, dummyPs)));
4.17 + val insts = take i dummyPs @ (P::(drop (i + 1) dummyPs));
4.18 val cert = cterm_of thy;
4.19 val insts' = (map cert induct_Ps) ~~ (map cert insts);
4.20 val induct' = refl RS ((nth
4.21 @@ -98,7 +98,7 @@
4.22 val descr' = flat descr;
4.23 val recTs = get_rec_types descr' sorts;
4.24 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
4.25 - val newTs = (uncurry take) (length (hd descr), recTs);
4.26 + val newTs = take (length (hd descr)) recTs;
4.27
4.28 val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
4.29
4.30 @@ -283,7 +283,7 @@
4.31 val descr' = flat descr;
4.32 val recTs = get_rec_types descr' sorts;
4.33 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
4.34 - val newTs = (uncurry take) (length (hd descr), recTs);
4.35 + val newTs = take (length (hd descr)) recTs;
4.36 val T' = TFree (Name.variant used "'t", HOLogic.typeS);
4.37
4.38 fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
4.39 @@ -305,8 +305,8 @@
4.40 let
4.41 val Ts = map (typ_of_dtyp descr' sorts) cargs;
4.42 val Ts' = Ts @ map mk_dummyT (filter is_rec_type cargs);
4.43 - val frees' = map (uncurry (mk_Free "x")) (Ts' ~~ (1 upto length Ts'));
4.44 - val frees = (uncurry take) (length cargs, frees');
4.45 + val frees' = map2 (mk_Free "x") Ts' (1 upto length Ts');
4.46 + val frees = take (length cargs) frees';
4.47 val free = mk_Free "f" (Ts ---> T') j
4.48 in
4.49 (free, list_abs_free (map dest_Free frees',
4.50 @@ -314,14 +314,14 @@
4.51 end) (constrs ~~ (1 upto length constrs)));
4.52
4.53 val caseT = (map (snd o dest_Free) fns1) @ [T] ---> T';
4.54 - val fns = flat ((uncurry take) (i, case_dummy_fns)) @
4.55 - fns2 @ flat ((uncurry drop) (i + 1, case_dummy_fns));
4.56 + val fns = flat (take i case_dummy_fns) @
4.57 + fns2 @ flat (drop (i + 1) case_dummy_fns);
4.58 val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
4.59 val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
4.60 val def = (Binding.name (Long_Name.base_name name ^ "_def"),
4.61 Logic.mk_equals (list_comb (Const (name, caseT), fns1),
4.62 - list_comb (reccomb, (flat ((uncurry take) (i, case_dummy_fns))) @
4.63 - fns2 @ (flat ((uncurry drop) (i + 1, case_dummy_fns))) )));
4.64 + list_comb (reccomb, (flat (take i case_dummy_fns)) @
4.65 + fns2 @ (flat (drop (i + 1) case_dummy_fns)))));
4.66 val ([def_thm], thy') =
4.67 thy
4.68 |> Sign.declare_const decl |> snd
4.69 @@ -329,7 +329,7 @@
4.70
4.71 in (defs @ [def_thm], thy')
4.72 end) (hd descr ~~ newTs ~~ case_names ~~
4.73 - (uncurry take) (length newTs, reccomb_names)) ([], thy1)
4.74 + take (length newTs) reccomb_names) ([], thy1)
4.75 ||> Theory.checkpoint;
4.76
4.77 val case_thms = map (map (fn t => Skip_Proof.prove_global thy2 [] [] t
4.78 @@ -353,7 +353,7 @@
4.79
4.80 val descr' = flat descr;
4.81 val recTs = get_rec_types descr' sorts;
4.82 - val newTs = (uncurry take) (length (hd descr), recTs);
4.83 + val newTs = take (length (hd descr)) recTs;
4.84
4.85 fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
4.86 exhaustion), case_thms'), T) =
5.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Nov 24 17:28:44 2009 +0100
5.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Nov 25 09:13:46 2009 +0100
5.3 @@ -217,19 +217,19 @@
5.4 invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
5.5 else
5.6 let
5.7 - val ts1 = (uncurry take) (i, ts);
5.8 - val t :: ts2 = (uncurry drop) (i, ts);
5.9 + val ts1 = take i ts;
5.10 + val t :: ts2 = drop i ts;
5.11 val names = List.foldr OldTerm.add_term_names
5.12 (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
5.13 - val (Ts, dT) = split_last ((uncurry take) (i+1, fst (strip_type T)));
5.14 + val (Ts, dT) = split_last (take (i+1) (fst (strip_type T)));
5.15
5.16 fun pcase [] [] [] gr = ([], gr)
5.17 | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
5.18 let
5.19 val j = length cargs;
5.20 val xs = Name.variant_list names (replicate j "x");
5.21 - val Us' = (uncurry take) (j, fst (strip_type U));
5.22 - val frees = map Free (xs ~~ Us');
5.23 + val Us' = take j (fst (strip_type U));
5.24 + val frees = map2 (curry Free) xs Us';
5.25 val (cp, gr0) = invoke_codegen thy defs dep module false
5.26 (list_comb (Const (cname, Us' ---> dT), frees)) gr;
5.27 val t' = Envir.beta_norm (list_comb (t, frees));
6.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML Tue Nov 24 17:28:44 2009 +0100
6.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Nov 25 09:13:46 2009 +0100
6.3 @@ -72,7 +72,7 @@
6.4 end;
6.5 in
6.6 map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
6.7 - (hd descr) ((uncurry take) (length (hd descr), get_rec_types descr' sorts))
6.8 + (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts))
6.9 end;
6.10
6.11
6.12 @@ -82,7 +82,7 @@
6.13 let
6.14 val descr' = flat descr;
6.15 val recTs = get_rec_types descr' sorts;
6.16 - val newTs = (uncurry take) (length (hd descr), recTs);
6.17 + val newTs = take (length (hd descr)) recTs;
6.18
6.19 fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
6.20
6.21 @@ -168,14 +168,12 @@
6.22 HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
6.23 end;
6.24
6.25 - fun make_casedist ((_, (_, _, constrs)), T) =
6.26 + fun make_casedist ((_, (_, _, constrs))) T =
6.27 let val prems = map (make_casedist_prem T) constrs
6.28 in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT)))
6.29 end
6.30
6.31 - in map make_casedist
6.32 - ((hd descr) ~~ (uncurry take) (length (hd descr), get_rec_types descr' sorts))
6.33 - end;
6.34 + in map2 make_casedist (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts)) end;
6.35
6.36 (*************** characteristic equations for primrec combinator **************)
6.37
6.38 @@ -257,7 +255,7 @@
6.39 val descr' = flat descr;
6.40 val recTs = get_rec_types descr' sorts;
6.41 val used = List.foldr OldTerm.add_typ_tfree_names [] recTs;
6.42 - val newTs = (uncurry take) (length (hd descr), recTs);
6.43 + val newTs = take (length (hd descr)) recTs;
6.44 val T' = TFree (Name.variant used "'t", HOLogic.typeS);
6.45
6.46 val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
6.47 @@ -280,7 +278,7 @@
6.48 let
6.49 val descr' = flat descr;
6.50 val recTs = get_rec_types descr' sorts;
6.51 - val newTs = (uncurry take) (length (hd descr), recTs);
6.52 + val newTs = take (length (hd descr)) recTs;
6.53
6.54 fun make_case T comb_t ((cname, cargs), f) =
6.55 let
6.56 @@ -304,7 +302,7 @@
6.57 val descr' = flat descr;
6.58 val recTs = get_rec_types descr' sorts;
6.59 val used' = List.foldr OldTerm.add_typ_tfree_names [] recTs;
6.60 - val newTs = (uncurry take) (length (hd descr), recTs);
6.61 + val newTs = take (length (hd descr)) recTs;
6.62 val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
6.63 val P = Free ("P", T' --> HOLogic.boolT);
6.64
6.65 @@ -415,7 +413,7 @@
6.66 let
6.67 val descr' = flat descr;
6.68 val recTs = get_rec_types descr' sorts;
6.69 - val newTs = (uncurry take) (length (hd descr), recTs);
6.70 + val newTs = take (length (hd descr)) recTs;
6.71
6.72 fun mk_eqn T (cname, cargs) =
6.73 let
7.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Nov 24 17:28:44 2009 +0100
7.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Nov 25 09:13:46 2009 +0100
7.3 @@ -77,8 +77,7 @@
7.4 subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
7.5 val leafTs = leafTs' @ map (fn n => TFree (n, (the o AList.lookup (op =) sorts) n)) unneeded_vars;
7.6 val recTs = get_rec_types descr' sorts;
7.7 - val newTs = (uncurry take) (length (hd descr), recTs);
7.8 - val oldTs = (uncurry drop) (length (hd descr), recTs);
7.9 + val (newTs, oldTs) = chop (length (hd descr)) recTs;
7.10 val sumT = if null leafTs then HOLogic.unitT
7.11 else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
7.12 val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
7.13 @@ -193,7 +192,7 @@
7.14 QUIET_BREADTH_FIRST (has_fewer_prems 1)
7.15 (resolve_tac rep_intrs 1)))
7.16 (types_syntax ~~ tyvars ~~
7.17 - ((uncurry take) (length newTs, rep_set_names)) ~~ new_type_names) ||>
7.18 + (take (length newTs) rep_set_names) ~~ new_type_names) ||>
7.19 Sign.add_path big_name;
7.20
7.21 (*********************** definition of constructors ***********************)
7.22 @@ -472,7 +471,7 @@
7.23 iso_inj_thms_unfolded;
7.24
7.25 val iso_thms = if length descr = 1 then [] else
7.26 - (uncurry drop) (length newTs, split_conj_thm
7.27 + drop (length newTs) (split_conj_thm
7.28 (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
7.29 [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
7.30 REPEAT (rtac TrueI 1),
8.1 --- a/src/HOL/Tools/Function/fun.ML Tue Nov 24 17:28:44 2009 +0100
8.2 +++ b/src/HOL/Tools/Function/fun.ML Wed Nov 25 09:13:46 2009 +0100
8.3 @@ -121,9 +121,9 @@
8.4 (Function_Split.split_all_equations ctxt compleqs)
8.5
8.6 fun restore_spec thms =
8.7 - bnds ~~ (uncurry take) (length bnds, Library.unflat spliteqs thms)
8.8 + bnds ~~ take (length bnds) (unflat spliteqs thms)
8.9
8.10 - val spliteqs' = flat ((uncurry take) (length bnds, spliteqs))
8.11 + val spliteqs' = flat (take (length bnds) spliteqs)
8.12 val fnames = map (fst o fst) fixes
8.13 val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs'
8.14
9.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Nov 24 17:28:44 2009 +0100
9.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Nov 25 09:13:46 2009 +0100
9.3 @@ -899,7 +899,7 @@
9.4 val (qs,p) = isolate_monomials vars eq
9.5 val rs = ideal (qs @ ps) p
9.6 (fn (s,t) => TermOrd.term_ord (term_of s, term_of t))
9.7 - in (eq,(uncurry take) (length qs, rs) ~~ vars)
9.8 + in (eq, take (length qs) rs ~~ vars)
9.9 end;
9.10 fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
9.11 in
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Nov 24 17:28:44 2009 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Nov 25 09:13:46 2009 +0100
10.3 @@ -496,7 +496,7 @@
10.4 bisim_depths mono_Ts nonmono_Ts
10.5 val ranks = map rank_of_block blocks
10.6 val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
10.7 - val head = (uncurry take) (max_scopes, all)
10.8 + val head = take max_scopes all
10.9 val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
10.10 head
10.11 in
11.1 --- a/src/HOL/Tools/inductive.ML Tue Nov 24 17:28:44 2009 +0100
11.2 +++ b/src/HOL/Tools/inductive.ML Wed Nov 25 09:13:46 2009 +0100
11.3 @@ -217,7 +217,7 @@
11.4 fun make_bool_args' xs =
11.5 make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
11.6
11.7 -fun arg_types_of k c = (uncurry drop) (k, binder_types (fastype_of c));
11.8 +fun arg_types_of k c = drop k (binder_types (fastype_of c));
11.9
11.10 fun find_arg T x [] = sys_error "find_arg"
11.11 | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
12.1 --- a/src/HOL/Tools/inductive_realizer.ML Tue Nov 24 17:28:44 2009 +0100
12.2 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Nov 25 09:13:46 2009 +0100
12.3 @@ -67,7 +67,7 @@
12.4 val Tvs = map TVar iTs;
12.5 val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
12.6 (Logic.strip_imp_concl (prop_of (hd intrs))));
12.7 - val params = map dest_Var ((uncurry take) (nparms, ts));
12.8 + val params = map dest_Var (take nparms ts);
12.9 val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
12.10 fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
12.11 map (Logic.unvarifyT o snd) (subtract (op =) params (rev (Term.add_vars (prop_of intr) []))) @
13.1 --- a/src/HOL/Tools/old_primrec.ML Tue Nov 24 17:28:44 2009 +0100
13.2 +++ b/src/HOL/Tools/old_primrec.ML Wed Nov 25 09:13:46 2009 +0100
13.3 @@ -124,8 +124,8 @@
13.4 let
13.5 val fnameT' as (fname', _) = dest_Const f;
13.6 val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
13.7 - val ls = (uncurry take) (rpos, ts);
13.8 - val rest = (uncurry drop) (rpos, ts);
13.9 + val ls = take rpos ts;
13.10 + val rest = drop rpos ts;
13.11 val (x', rs) = (hd rest, tl rest)
13.12 handle Empty => raise RecError ("not enough arguments\
13.13 \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
14.1 --- a/src/HOL/Tools/record.ML Tue Nov 24 17:28:44 2009 +0100
14.2 +++ b/src/HOL/Tools/record.ML Wed Nov 25 09:13:46 2009 +0100
14.3 @@ -321,7 +321,7 @@
14.4 fun rec_id i T =
14.5 let
14.6 val rTs = dest_recTs T;
14.7 - val rTs' = if i < 0 then rTs else (uncurry take) (i, rTs);
14.8 + val rTs' = if i < 0 then rTs else take i rTs;
14.9 in implode (map #1 rTs') end;
14.10
14.11
14.12 @@ -1582,7 +1582,7 @@
14.13 (Logic.strip_assums_concl (prop_of rule')));
14.14 (*ca indicates if rule is a case analysis or induction rule*)
14.15 val (x, ca) =
14.16 - (case rev ((uncurry drop) (length params, ys)) of
14.17 + (case rev (drop (length params) ys) of
14.18 [] => (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
14.19 (hd (rev (Logic.strip_assums_hyp (hd (prems_of rule')))))))), true)
14.20 | [x] => (head_of x, false));
14.21 @@ -1635,7 +1635,7 @@
14.22 else if len > 16 then
14.23 let
14.24 fun group16 [] = []
14.25 - | group16 xs = (uncurry take) (16, xs) :: group16 ((uncurry drop) (16, xs));
14.26 + | group16 xs = take 16 xs :: group16 (drop 16 xs);
14.27 val vars' = group16 vars;
14.28 val (composites, (thy', i')) = fold_map mk_even_istuple vars' (thy, i);
14.29 in
14.30 @@ -1772,7 +1772,7 @@
14.31
14.32 fun chunks [] [] = []
14.33 | chunks [] xs = [xs]
14.34 - | chunks (l :: ls) xs = (uncurry take) (l, xs) :: chunks ls ((uncurry drop) (l, xs));
14.35 + | chunks (l :: ls) xs = take l xs :: chunks ls (drop l xs);
14.36
14.37 fun chop_last [] = error "chop_last: list should not be empty"
14.38 | chop_last [x] = ([], x)
14.39 @@ -1881,12 +1881,12 @@
14.40 val extension_names = map (unsuffix ext_typeN o fst o #extension) parents @ [extN];
14.41 val extension_id = implode extension_names;
14.42
14.43 - fun rec_schemeT n = mk_recordT (map #extension ((uncurry drop) (n, parents))) extT;
14.44 + fun rec_schemeT n = mk_recordT (map #extension (drop n parents)) extT;
14.45 val rec_schemeT0 = rec_schemeT 0;
14.46
14.47 fun recT n =
14.48 let val (c, Ts) = extension in
14.49 - mk_recordT (map #extension ((uncurry drop) (n, parents)))
14.50 + mk_recordT (map #extension (drop n parents))
14.51 (Type (c, subst_last HOLogic.unitT Ts))
14.52 end;
14.53 val recT0 = recT 0;
14.54 @@ -1896,7 +1896,7 @@
14.55 val (args', more) = chop_last args;
14.56 fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
14.57 fun build Ts =
14.58 - fold_rev mk_ext' ((uncurry drop) (n, (extension_names ~~ Ts) ~~ chunks parent_chunks args'))
14.59 + fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args'))
14.60 more;
14.61 in
14.62 if more = HOLogic.unit
14.63 @@ -1989,7 +1989,7 @@
14.64 val (accessor_thms, updator_thms, upd_acc_cong_assists) =
14.65 timeit_msg "record getting tree access/updates:" get_access_update_thms;
14.66
14.67 - fun lastN xs = (uncurry drop) (parent_fields_len, xs);
14.68 + fun lastN xs = drop parent_fields_len xs;
14.69
14.70 (*selectors*)
14.71 fun mk_sel_spec ((c, T), thm) =
15.1 --- a/src/HOL/Tools/split_rule.ML Tue Nov 24 17:28:44 2009 +0100
15.2 +++ b/src/HOL/Tools/split_rule.ML Wed Nov 25 09:13:46 2009 +0100
15.3 @@ -74,8 +74,8 @@
15.4 let
15.5 val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
15.6 val (Us', U') = strip_type T;
15.7 - val Us = (uncurry take) (length ts, Us');
15.8 - val U = (uncurry drop) (length ts, Us') ---> U';
15.9 + val Us = take (length ts) Us';
15.10 + val U = drop (length ts) Us' ---> U';
15.11 val T' = maps HOLogic.flatten_tupleT Us ---> U;
15.12 fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
15.13 let
16.1 --- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Nov 24 17:28:44 2009 +0100
16.2 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Nov 25 09:13:46 2009 +0100
16.3 @@ -153,7 +153,7 @@
16.4 val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
16.5 val dts = map (Type o fst) eqs';
16.6 val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
16.7 - fun strip ss = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
16.8 + fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
16.9 fun typid (Type (id,_)) =
16.10 let val c = hd (Symbol.explode (Long_Name.base_name id))
16.11 in if Symbol.is_letter c then c else "t" end
16.12 @@ -228,7 +228,7 @@
16.13 val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
16.14 val dts = map (Type o fst) eqs';
16.15 val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
16.16 - fun strip ss = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
16.17 + fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
16.18 fun typid (Type (id,_)) =
16.19 let val c = hd (Symbol.explode (Long_Name.base_name id))
16.20 in if Symbol.is_letter c then c else "t" end
17.1 --- a/src/Pure/General/path.ML Tue Nov 24 17:28:44 2009 +0100
17.2 +++ b/src/Pure/General/path.ML Wed Nov 25 09:13:46 2009 +0100
17.3 @@ -139,7 +139,7 @@
17.4 val split_ext = split_path (fn (prfx, s) => apfst (append (Path prfx))
17.5 (case take_suffix (fn c => c <> ".") (explode s) of
17.6 ([], _) => (Path [Basic s], "")
17.7 - | (cs, e) => (Path [Basic (implode ((uncurry take) (length cs - 1, cs)))], implode e)));
17.8 + | (cs, e) => (Path [Basic (implode (take (length cs - 1) cs))], implode e)));
17.9
17.10
17.11 (* expand variables *)
18.1 --- a/src/Pure/General/scan.ML Tue Nov 24 17:28:44 2009 +0100
18.2 +++ b/src/Pure/General/scan.ML Wed Nov 25 09:13:46 2009 +0100
18.3 @@ -221,7 +221,7 @@
18.4
18.5 fun trace scan xs =
18.6 let val (y, xs') = scan xs
18.7 - in ((y, (uncurry take) (length xs - length xs', xs)), xs') end;
18.8 + in ((y, take (length xs - length xs') xs), xs') end;
18.9
18.10
18.11 (* stopper *)
19.1 --- a/src/Pure/Isar/code.ML Tue Nov 24 17:28:44 2009 +0100
19.2 +++ b/src/Pure/Isar/code.ML Wed Nov 25 09:13:46 2009 +0100
19.3 @@ -128,7 +128,7 @@
19.4 val args = args_of thm;
19.5 val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
19.6 fun matches_args args' = length args <= length args' andalso
19.7 - Pattern.matchess thy (args, (map incr_idx o curry (uncurry take) (length args)) args');
19.8 + Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
19.9 fun drop (thm', proper') = if (proper orelse not proper')
19.10 andalso matches_args (args_of thm') then
19.11 (warning ("Code generator: dropping redundant code equation\n" ^
20.1 --- a/src/Pure/Isar/obtain.ML Tue Nov 24 17:28:44 2009 +0100
20.2 +++ b/src/Pure/Isar/obtain.ML Wed Nov 25 09:13:46 2009 +0100
20.3 @@ -232,12 +232,12 @@
20.4 err ("Failed to unify variable " ^
20.5 string_of_term (Free (x, Envir.norm_type tyenv T)) ^ " against parameter " ^
20.6 string_of_term (Syntax.mark_boundT (y, Envir.norm_type tyenv U)) ^ " in") rule;
20.7 - val (tyenv, _) = fold unify (map #1 vars ~~ (uncurry take) (m, params))
20.8 + val (tyenv, _) = fold unify (map #1 vars ~~ take m params)
20.9 (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
20.10 val norm_type = Envir.norm_type tyenv;
20.11
20.12 val xs = map (apsnd norm_type o fst) vars;
20.13 - val ys = map (apsnd norm_type) ((uncurry drop) (m, params));
20.14 + val ys = map (apsnd norm_type) (drop m params);
20.15 val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
20.16 val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
20.17
21.1 --- a/src/Pure/Isar/proof_context.ML Tue Nov 24 17:28:44 2009 +0100
21.2 +++ b/src/Pure/Isar/proof_context.ML Wed Nov 25 09:13:46 2009 +0100
21.3 @@ -1340,7 +1340,7 @@
21.4 val suppressed = len - ! prems_limit;
21.5 val prt_prems = if null prems then []
21.6 else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
21.7 - map (Display.pretty_thm ctxt) ((uncurry drop) (suppressed, prems)))];
21.8 + map (Display.pretty_thm ctxt) (drop suppressed prems))];
21.9 in prt_structs @ prt_fixes @ prt_prems end;
21.10
21.11
22.1 --- a/src/Pure/Isar/rule_cases.ML Tue Nov 24 17:28:44 2009 +0100
22.2 +++ b/src/Pure/Isar/rule_cases.ML Wed Nov 25 09:13:46 2009 +0100
22.3 @@ -144,7 +144,7 @@
22.4 (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
22.5 NONE => (name, NONE)
22.6 | SOME p => (name, extract_case is_open thy p name concls)) :: cs, i - 1);
22.7 - in fold_rev add_case ((uncurry drop) (n - nprems, cases)) ([], n) |> #1 end;
22.8 + in fold_rev add_case (drop (n - nprems) cases) ([], n) |> #1 end;
22.9
22.10 in
22.11
22.12 @@ -205,8 +205,8 @@
22.13 th
22.14 |> unfold_prems n defs
22.15 |> unfold_prems_concls defs
22.16 - |> Drule.multi_resolve ((uncurry take) (m, facts))
22.17 - |> Seq.map (pair (xx, (n - m, (uncurry drop) (m, facts))))
22.18 + |> Drule.multi_resolve (take m facts)
22.19 + |> Seq.map (pair (xx, (n - m, drop m facts)))
22.20 end;
22.21
22.22 end;
22.23 @@ -345,7 +345,7 @@
22.24 fun prep_rule n th =
22.25 let
22.26 val th' = Thm.permute_prems 0 n th;
22.27 - val prems = (uncurry take) (Thm.nprems_of th' - n, Drule.cprems_of th');
22.28 + val prems = take (Thm.nprems_of th' - n) (Drule.cprems_of th');
22.29 val th'' = Drule.implies_elim_list th' (map Thm.assume prems);
22.30 in (prems, (n, th'')) end;
22.31
23.1 --- a/src/Pure/Proof/extraction.ML Tue Nov 24 17:28:44 2009 +0100
23.2 +++ b/src/Pure/Proof/extraction.ML Wed Nov 25 09:13:46 2009 +0100
23.3 @@ -461,7 +461,7 @@
23.4 end
23.5 else (vs', tye)
23.6
23.7 - in fold_rev add_args ((uncurry take) (n, vars) ~~ (uncurry take) (n, ts)) ([], []) end;
23.8 + in fold_rev add_args (take n vars ~~ take n ts) ([], []) end;
23.9
23.10 fun find (vs: string list) = Option.map snd o find_first (curry (eq_set (op =)) vs o fst);
23.11 fun find' (s: string) = map_filter (fn (s', x) => if s = s' then SOME x else NONE);
24.1 --- a/src/Pure/Syntax/ast.ML Tue Nov 24 17:28:44 2009 +0100
24.2 +++ b/src/Pure/Syntax/ast.ML Wed Nov 25 09:13:46 2009 +0100
24.3 @@ -158,7 +158,7 @@
24.4 (case (ast, pat) of
24.5 (Appl asts, Appl pats) =>
24.6 let val a = length asts and p = length pats in
24.7 - if a > p then (Appl ((uncurry take) (p, asts)), (uncurry drop) (p, asts))
24.8 + if a > p then (Appl (take p asts), drop p asts)
24.9 else (ast, [])
24.10 end
24.11 | _ => (ast, []));
25.1 --- a/src/Pure/Syntax/syntax.ML Tue Nov 24 17:28:44 2009 +0100
25.2 +++ b/src/Pure/Syntax/syntax.ML Wed Nov 25 09:13:46 2009 +0100
25.3 @@ -499,7 +499,7 @@
25.4 (("Ambiguous input" ^ Position.str_of pos ^
25.5 "\nproduces " ^ string_of_int len ^ " parse trees" ^
25.6 (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
25.7 - map show_pt ((uncurry take) (limit, pts)))));
25.8 + map show_pt (take limit pts))));
25.9 SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
25.10 end;
25.11
25.12 @@ -545,7 +545,7 @@
25.13 else cat_error (ambig_msg ()) (cat_lines
25.14 (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
25.15 (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
25.16 - map (Pretty.string_of_term pp) ((uncurry take) (limit, results))))
25.17 + map (Pretty.string_of_term pp) (take limit results)))
25.18 end;
25.19
25.20 fun standard_parse_term pp check get_sort map_const map_free map_type map_sort
26.1 --- a/src/Pure/Thy/present.ML Tue Nov 24 17:28:44 2009 +0100
26.2 +++ b/src/Pure/Thy/present.ML Wed Nov 25 09:13:46 2009 +0100
26.3 @@ -285,7 +285,7 @@
26.4 (browser_info := empty_browser_info; session_info := NONE)
26.5 else
26.6 let
26.7 - val parent_name = name_of_session ((uncurry take) (length path - 1, path));
26.8 + val parent_name = name_of_session (take (length path - 1) path);
26.9 val session_name = name_of_session path;
26.10 val sess_prefix = Path.make path;
26.11 val html_prefix = Path.append (Path.expand output_path) sess_prefix;
27.1 --- a/src/Pure/Thy/thy_output.ML Tue Nov 24 17:28:44 2009 +0100
27.2 +++ b/src/Pure/Thy/thy_output.ML Wed Nov 25 09:13:46 2009 +0100
27.3 @@ -265,7 +265,7 @@
27.4 if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
27.5 else if nesting >= 0 then (tag', replicate nesting tag @ tags)
27.6 else
27.7 - (case (uncurry drop) (~ nesting - 1, tags) of
27.8 + (case drop (~ nesting - 1) tags of
27.9 tgs :: tgss => (tgs, tgss)
27.10 | [] => err_bad_nesting (Position.str_of cmd_pos));
27.11
28.1 --- a/src/Pure/Tools/find_theorems.ML Tue Nov 24 17:28:44 2009 +0100
28.2 +++ b/src/Pure/Tools/find_theorems.ML Wed Nov 25 09:13:46 2009 +0100
28.3 @@ -409,7 +409,7 @@
28.4
28.5 val len = length matches;
28.6 val lim = the_default (! limit) opt_limit;
28.7 - in (SOME len, (uncurry drop) (len - lim, matches)) end;
28.8 + in (SOME len, drop (len - lim) matches) end;
28.9
28.10 val find =
28.11 if rem_dups orelse is_none opt_limit
29.1 --- a/src/Pure/assumption.ML Tue Nov 24 17:28:44 2009 +0100
29.2 +++ b/src/Pure/assumption.ML Wed Nov 25 09:13:46 2009 +0100
29.3 @@ -88,12 +88,12 @@
29.4 (* local assumptions *)
29.5
29.6 fun local_assumptions_of inner outer =
29.7 - (uncurry drop) (length (all_assumptions_of outer), all_assumptions_of inner);
29.8 + drop (length (all_assumptions_of outer)) (all_assumptions_of inner);
29.9
29.10 val local_assms_of = maps #2 oo local_assumptions_of;
29.11
29.12 fun local_prems_of inner outer =
29.13 - (uncurry drop) (length (all_prems_of outer), all_prems_of inner);
29.14 + drop (length (all_prems_of outer)) (all_prems_of inner);
29.15
29.16
29.17 (* add assumptions *)
30.1 --- a/src/Pure/codegen.ML Tue Nov 24 17:28:44 2009 +0100
30.2 +++ b/src/Pure/codegen.ML Wed Nov 25 09:13:46 2009 +0100
30.3 @@ -579,11 +579,11 @@
30.4 fun eta_expand t ts i =
30.5 let
30.6 val k = length ts;
30.7 - val Ts = (uncurry drop) (k, binder_types (fastype_of t));
30.8 + val Ts = drop k (binder_types (fastype_of t));
30.9 val j = i - k
30.10 in
30.11 List.foldr (fn (T, t) => Abs ("x", T, t))
30.12 - (list_comb (t, ts @ map Bound (j-1 downto 0))) ((uncurry take) (j, Ts))
30.13 + (list_comb (t, ts @ map Bound (j-1 downto 0))) (take j Ts)
30.14 end;
30.15
30.16 fun mk_app _ p [] = p
31.1 --- a/src/Pure/goal_display.ML Tue Nov 24 17:28:44 2009 +0100
31.2 +++ b/src/Pure/goal_display.ML Wed Nov 25 09:13:46 2009 +0100
31.3 @@ -99,7 +99,7 @@
31.4 (if main then [prt_term B] else []) @
31.5 (if ngoals = 0 then [Pretty.str "No subgoals!"]
31.6 else if ngoals > maxgoals then
31.7 - pretty_subgoals ((uncurry take) (maxgoals, As)) @
31.8 + pretty_subgoals (take maxgoals As) @
31.9 (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
31.10 else [])
31.11 else pretty_subgoals As) @
32.1 --- a/src/Pure/meta_simplifier.ML Tue Nov 24 17:28:44 2009 +0100
32.2 +++ b/src/Pure/meta_simplifier.ML Wed Nov 25 09:13:46 2009 +0100
32.3 @@ -1163,9 +1163,9 @@
32.4 val (rrs', asm') = rules_of_prem ss prem'
32.5 in mut_impc prems concl rrss asms (prem' :: prems')
32.6 (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
32.7 - ((uncurry take) (i, prems))
32.8 + (take i prems)
32.9 (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
32.10 - ((uncurry drop) (i, prems), concl))))) :: eqns)
32.11 + (drop i prems, concl))))) :: eqns)
32.12 ss (length prems') ~1
32.13 end
32.14
33.1 --- a/src/Pure/proofterm.ML Tue Nov 24 17:28:44 2009 +0100
33.2 +++ b/src/Pure/proofterm.ML Wed Nov 25 09:13:46 2009 +0100
33.3 @@ -1003,7 +1003,7 @@
33.4 | _ => error "shrink: proof not in normal form");
33.5 val vs = vars_of prop;
33.6 val (ts', ts'') = chop (length vs) ts;
33.7 - val insts = (uncurry take) (length ts', map (fst o dest_Var) vs) ~~ ts';
33.8 + val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts';
33.9 val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
33.10 insert (op =) ixn (case AList.lookup (op =) insts ixn of
33.11 SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
34.1 --- a/src/Pure/tactic.ML Tue Nov 24 17:28:44 2009 +0100
34.2 +++ b/src/Pure/tactic.ML Wed Nov 25 09:13:46 2009 +0100
34.3 @@ -173,7 +173,7 @@
34.4 perm_tac 0 (1 - i);
34.5
34.6 fun distinct_subgoal_tac i st =
34.7 - (case (uncurry drop) (i - 1, Thm.prems_of st) of
34.8 + (case drop (i - 1) (Thm.prems_of st) of
34.9 [] => no_tac st
34.10 | A :: Bs =>
34.11 st |> EVERY (fold (fn (B, k) =>
35.1 --- a/src/Pure/thm.ML Tue Nov 24 17:28:44 2009 +0100
35.2 +++ b/src/Pure/thm.ML Wed Nov 25 09:13:46 2009 +0100
35.3 @@ -1457,7 +1457,7 @@
35.4 val short = length iparams - length cs;
35.5 val newnames =
35.6 if short < 0 then error "More names than abstractions!"
35.7 - else Name.variant_list cs ((uncurry take) (short, iparams)) @ cs;
35.8 + else Name.variant_list cs (take short iparams) @ cs;
35.9 val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
35.10 val newBi = Logic.list_rename_params (newnames, Bi);
35.11 in
36.1 --- a/src/Pure/variable.ML Tue Nov 24 17:28:44 2009 +0100
36.2 +++ b/src/Pure/variable.ML Wed Nov 25 09:13:46 2009 +0100
36.3 @@ -345,7 +345,7 @@
36.4 val fixes_inner = fixes_of inner;
36.5 val fixes_outer = fixes_of outer;
36.6
36.7 - val gen_fixes = map #2 ((uncurry take) (length fixes_inner - length fixes_outer, fixes_inner));
36.8 + val gen_fixes = map #2 (take (length fixes_inner - length fixes_outer) fixes_inner);
36.9 val still_fixed = not o member (op =) gen_fixes;
36.10
36.11 val type_occs_inner = type_occs_of inner;
37.1 --- a/src/Tools/Code/code_haskell.ML Tue Nov 24 17:28:44 2009 +0100
37.2 +++ b/src/Tools/Code/code_haskell.ML Wed Nov 25 09:13:46 2009 +0100
37.3 @@ -78,7 +78,7 @@
37.4 and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
37.5 of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
37.6 | fingerprint => let
37.7 - val ts_fingerprint = ts ~~ curry (uncurry take) (length ts) fingerprint;
37.8 + val ts_fingerprint = ts ~~ take (length ts) fingerprint;
37.9 val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
37.10 (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
37.11 fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t
37.12 @@ -86,7 +86,7 @@
37.13 brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty];
37.14 in
37.15 if needs_annotation then
37.16 - (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry (uncurry take) (length ts) tys)
37.17 + (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (take (length ts) tys)
37.18 else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
37.19 end
37.20 and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
38.1 --- a/src/Tools/Code/code_printer.ML Tue Nov 24 17:28:44 2009 +0100
38.2 +++ b/src/Tools/Code/code_printer.ML Wed Nov 25 09:13:46 2009 +0100
38.3 @@ -231,7 +231,7 @@
38.4 of NONE => brackify fxy (pr_app thm vars app)
38.5 | SOME (k, pr) =>
38.6 let
38.7 - fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry (uncurry take) k tys);
38.8 + fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ take k tys);
38.9 in if k = length ts
38.10 then pr' fxy ts
38.11 else if k < length ts
39.1 --- a/src/Tools/Code/code_thingol.ML Tue Nov 24 17:28:44 2009 +0100
39.2 +++ b/src/Tools/Code/code_thingol.ML Wed Nov 25 09:13:46 2009 +0100
39.3 @@ -226,7 +226,7 @@
39.4 val l = k - j;
39.5 val ctxt = (fold o fold_varnames) Name.declare ts Name.context;
39.6 val vs_tys = (map o apfst) SOME
39.7 - (Name.names ctxt "a" ((curry (uncurry take) l o curry (uncurry drop) j) tys));
39.8 + (Name.names ctxt "a" ((take l o drop j) tys));
39.9 in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
39.10
39.11 fun contains_dictvar t =
39.12 @@ -773,7 +773,7 @@
39.13 val clauses = if null case_pats
39.14 then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
39.15 else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
39.16 - mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry (uncurry take) n tys) t)
39.17 + mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
39.18 (constrs ~~ ts_clause);
39.19 in ((t, ty), clauses) end;
39.20 in
39.21 @@ -788,7 +788,7 @@
39.22 if length ts < num_args then
39.23 let
39.24 val k = length ts;
39.25 - val tys = (curry (uncurry take) (num_args - k) o curry (uncurry drop) k o fst o strip_type) ty;
39.26 + val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
39.27 val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
39.28 val vs = Name.names ctxt "a" tys;
39.29 in
39.30 @@ -797,8 +797,8 @@
39.31 #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
39.32 end
39.33 else if length ts > num_args then
39.34 - translate_case thy algbr eqngr thm case_scheme ((c, ty), (uncurry take) (num_args, ts))
39.35 - ##>> fold_map (translate_term thy algbr eqngr thm) ((uncurry drop) (num_args, ts))
39.36 + translate_case thy algbr eqngr thm case_scheme ((c, ty), take num_args ts)
39.37 + ##>> fold_map (translate_term thy algbr eqngr thm) (drop num_args ts)
39.38 #>> (fn (t, ts) => t `$$ ts)
39.39 else
39.40 translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
40.1 --- a/src/Tools/induct.ML Tue Nov 24 17:28:44 2009 +0100
40.2 +++ b/src/Tools/induct.ML Wed Nov 25 09:13:46 2009 +0100
40.3 @@ -280,11 +280,11 @@
40.4
40.5 fun align_left msg xs ys =
40.6 let val m = length xs and n = length ys
40.7 - in if m < n then error msg else ((uncurry take) (n, xs) ~~ ys) end;
40.8 + in if m < n then error msg else (take n xs ~~ ys) end;
40.9
40.10 fun align_right msg xs ys =
40.11 let val m = length xs and n = length ys
40.12 - in if m < n then error msg else ((uncurry drop) (m - n, xs) ~~ ys) end;
40.13 + in if m < n then error msg else (drop (m - n) xs ~~ ys) end;
40.14
40.15
40.16 (* prep_inst *)
41.1 --- a/src/Tools/induct_tacs.ML Tue Nov 24 17:28:44 2009 +0100
41.2 +++ b/src/Tools/induct_tacs.ML Wed Nov 25 09:13:46 2009 +0100
41.3 @@ -59,7 +59,7 @@
41.4
41.5 fun prep_inst (concl, xs) =
41.6 let val vs = Induct.vars_of concl
41.7 - in map_filter prep_var ((uncurry drop) (length vs - length xs, vs) ~~ xs) end;
41.8 + in map_filter prep_var (drop (length vs - length xs) vs ~~ xs) end;
41.9
41.10 in
41.11
42.1 --- a/src/ZF/Tools/cartprod.ML Tue Nov 24 17:28:44 2009 +0100
42.2 +++ b/src/ZF/Tools/cartprod.ML Wed Nov 25 09:13:46 2009 +0100
42.3 @@ -96,8 +96,8 @@
42.4
42.5 (*Makes a nested tuple from a list, following the product type structure*)
42.6 fun mk_tuple pair (Type("*", [T1,T2])) tms =
42.7 - pair $ (mk_tuple pair T1 tms)
42.8 - $ (mk_tuple pair T2 ((uncurry drop) (length (factors T1), tms)))
42.9 + pair $ mk_tuple pair T1 tms
42.10 + $ mk_tuple pair T2 (drop (length (factors T1)) tms)
42.11 | mk_tuple pair T (t::_) = t;
42.12
42.13 (*Attempts to remove occurrences of split, and pair-valued parameters*)