src/Pure/Isar/rule_cases.ML

 fun internalize_params rule =
   let
     fun rename prem =
       let val xs =
         map (Name.internal o Name.clean o fst) (Logic.strip_params prem)
-      in Logic.list_rename_params (xs, prem) end;
+      in Logic.list_rename_params xs 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;