clarified names context: proper context, without consts;

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