# HG changeset patch
# User wenzelm
# Date 1733084096 -3600
# Node ID 3e55334ef5afe50400126ed235ee2a247f64d6f7
# Parent  13e9678f2c00e67be8457de9ee053aa839b1a7cf
clarified names context: proper context, without consts;

diff -r 13e9678f2c00 -r 3e55334ef5af src/HOL/Tools/inductive.ML
--- 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);