diff -r 44c0028486db -r 31b05aef022d src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Nov 30 19:21:38 2024 +0100
@@ -245,9 +245,9 @@
              if null (preds_of ps prem) then prem
              else lift_prem prem) prems,
            HOLogic.mk_Trueprop (lift_pred p ts));
-        val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params')
+        val vs = map (Var o apfst (rpair 0)) (Term.variant_frees prem params')
       in
-        (Logic.list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
+        (Logic.list_all (params', prem), (vs, subst_bounds (rev vs, prem)))
       end) prems);
 
     val ind_vars =