src/Pure/Isar/rule_cases.ML

     fun add_case (name, concls) (cs, i) =
       ((case try (fn () =>
           (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
 
 fun make_common is_open = make is_open NONE;
 fun make_nested is_open rule_struct = make is_open (SOME rule_struct);

 fun consume defs facts ((xx, n), th) =
   let val m = Int.min (length facts, n) in
     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;
 
 val consumes_tagN = "consumes";

   is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us));
 
 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;
 
 in