--- a/src/HOL/Tools/inductive.ML Sun Dec 01 21:13:57 2024 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Dec 01 21:14:56 2024 +0100
@@ -338,7 +338,7 @@
fun check_rule ctxt cs params ((binding, att), rule) =
let
- val params' = Term.variant_frees rule (Logic.strip_params rule);
+ val params' = Variable.variant_names (Variable.declare_names rule ctxt) (Logic.strip_params rule);
val frees = rev (map Free params');
val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);