src/HOL/Nominal/nominal_induct.ML

       let
         val vars = Induct.vars_of concl;
         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)) ::
         map_filter (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ inst)
       end;

       let
         val ps = Logic.strip_params prem;
         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)
       in Logic.list_implies (map rename As, C) end;
   in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;