src/Tools/induct.ML

           let
             val xs = rename_params (Logic.strip_params A);
             val xs' =
               (case filter (fn x' => x' = x) xs of
                 [] => xs | [_] => xs | _ => index 1 xs);
-          in Logic.list_rename_params (xs', A) end;
+          in Logic.list_rename_params xs' A end;
         fun rename_prop p =
           let val (As, C) = Logic.strip_horn p
           in Logic.list_implies (map rename_asm As, C) end;
         val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
         val thm' = Thm.equal_elim (Thm.reflexive cp') thm;