src/HOL/Nominal/nominal_induct.ML

         val ps = Logic.strip_params prem;
         val p = length ps;
         val ys =
           if p < n then []
           else map (tune o #1) (take (p - n) ps) @ xs;
-      in Logic.list_rename_params (ys, prem) end;
+      in Logic.list_rename_params ys prem end;
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn prop
       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;