diff -r 44c0028486db -r 31b05aef022d src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Nov 30 19:21:38 2024 +0100
@@ -146,8 +146,8 @@
   in Option.map prove (map_term f prop (the_default prop opt)) end;
 
 fun abs_params params t =
-  let val vs =  map (Var o apfst (rpair 0)) (Term.rename_wrt_term t params)
-  in (Logic.list_all (params, t), (rev vs, subst_bounds (vs, t))) end;
+  let val vs =  map (Var o apfst (rpair 0)) (Term.variant_frees t params)
+  in (Logic.list_all (params, t), (vs, subst_bounds (rev vs, t))) end;
 
 fun inst_params thy (vs, p) th cts =
   let val env = Pattern.first_order_match thy (p, Thm.prop_of th)