--- 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)