clarified renaming of bounds, using Syntax_Trans.variant_bounds: avoid structures and fixed variables with syntax;

--- a/src/FOL/IFOL.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/FOL/IFOL.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -105,7 +105,7 @@
 syntax_consts "_Uniq" \<rightleftharpoons> Uniq
 translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
 typed_print_translation \<open>
-  [(\<^const_syntax>\<open>Uniq\<close>, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
+  [(\<^const_syntax>\<open>Uniq\<close>, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 

--- a/src/HOL/HOL.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/HOL.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -135,7 +135,7 @@
 translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
 
 typed_print_translation \<open>
-  [(\<^const_syntax>\<open>Uniq\<close>, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
+  [(\<^const_syntax>\<open>Uniq\<close>, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Uniq\<close>)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 
@@ -150,7 +150,7 @@
 translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
 
 typed_print_translation \<open>
-  [(\<^const_syntax>\<open>Ex1\<close>, fn _ => Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Ex1\<close>)]
+  [(\<^const_syntax>\<open>Ex1\<close>, Syntax_Trans.preserve_binder_abs_tr' \<^syntax_const>\<open>_Ex1\<close>)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 
@@ -183,8 +183,8 @@
 syntax_consts "_The" \<rightleftharpoons> The
 translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
 print_translation \<open>
-  [(\<^const_syntax>\<open>The\<close>, fn _ => fn [Abs abs] =>
-      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+  [(\<^const_syntax>\<open>The\<close>, fn ctxt => fn [Abs abs] =>
+      let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
       in Syntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)]
 \<close>  \<comment> \<open>To avoid eta-contraction of body\<close>
 

--- a/src/HOL/HOLCF/Cfun.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -39,8 +39,8 @@
 \<close>
 
 print_translation \<open>
-  [(\<^const_syntax>\<open>Abs_cfun\<close>, fn _ => fn [Abs abs] =>
-      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+  [(\<^const_syntax>\<open>Abs_cfun\<close>, fn ctxt => fn [Abs abs] =>
+      let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
       in Syntax.const \<^syntax_const>\<open>_cabs\<close> $ x $ t end)]
 \<close>  \<comment> \<open>To avoid eta-contraction of body\<close>
 

--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -142,29 +142,29 @@
 
 print_translation \<open>
   let
-    fun dest_LAM (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>unit_when\<close>,_) $ t) =
+    fun dest_LAM _ (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>unit_when\<close>,_) $ t) =
           (Syntax.const \<^syntax_const>\<open>_noargs\<close>, t)
-    |   dest_LAM (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>csplit\<close>,_) $ t) =
+    |   dest_LAM ctxt (Const (\<^const_syntax>\<open>Rep_cfun\<close>,_) $ Const (\<^const_syntax>\<open>csplit\<close>,_) $ t) =
           let
-            val (v1, t1) = dest_LAM t;
-            val (v2, t2) = dest_LAM t1;
+            val (v1, t1) = dest_LAM ctxt t;
+            val (v2, t2) = dest_LAM ctxt t1;
           in (Syntax.const \<^syntax_const>\<open>_args\<close> $ v1 $ v2, t2) end
-    |   dest_LAM (Const (\<^const_syntax>\<open>Abs_cfun\<close>,_) $ t) =
+    |   dest_LAM ctxt (Const (\<^const_syntax>\<open>Abs_cfun\<close>,_) $ t) =
           let
             val abs =
               case t of Abs abs => abs
                 | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
-            val (x, t') = Syntax_Trans.atomic_abs_tr' abs;
+            val (x, t') = Syntax_Trans.atomic_abs_tr' ctxt abs;
           in (Syntax.const \<^syntax_const>\<open>_variable\<close> $ x, t') end
-    |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
+    |   dest_LAM _ _ = raise Match; (* too few vars: abort translation *)
 
-    fun Case1_tr' [Const(\<^const_syntax>\<open>branch\<close>,_) $ p, r] =
-          let val (v, t) = dest_LAM r in
+    fun Case1_tr' ctxt [Const(\<^const_syntax>\<open>branch\<close>,_) $ p, r] =
+          let val (v, t) = dest_LAM ctxt r in
             Syntax.const \<^syntax_const>\<open>_Case1\<close> $
               (Syntax.const \<^syntax_const>\<open>_match\<close> $ p $ v) $ t
           end;
 
-  in [(\<^const_syntax>\<open>Rep_cfun\<close>, K Case1_tr')] end
+  in [(\<^const_syntax>\<open>Rep_cfun\<close>, Case1_tr')] end
 \<close>
 
 translations

--- a/src/HOL/Hilbert_Choice.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -29,8 +29,8 @@
   "SOME x. P" \<rightleftharpoons> "CONST Eps (\<lambda>x. P)"
 
 print_translation \<open>
-  [(\<^const_syntax>\<open>Eps\<close>, fn _ => fn [Abs abs] =>
-      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+  [(\<^const_syntax>\<open>Eps\<close>, fn ctxt => fn [Abs abs] =>
+      let val (x, t) = Syntax_Trans.atomic_abs_tr' ctxt abs
       in Syntax.const \<^syntax_const>\<open>_Eps\<close> $ x $ t end)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 

--- a/src/HOL/Library/FSet.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/Library/FSet.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -216,8 +216,8 @@
   "\<exists>!x|\<in>|A. P" \<rightharpoonup> "\<exists>!x. x |\<in>| A \<and> P"
 
 typed_print_translation \<open>
- [(\<^const_syntax>\<open>fBall\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBall\<close>),
-  (\<^const_syntax>\<open>fBex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBex\<close>)]
+ [(\<^const_syntax>\<open>fBall\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBall\<close>),
+  (\<^const_syntax>\<open>fBex\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_fBex\<close>)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 syntax

--- a/src/HOL/Library/Multiset.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -181,8 +181,8 @@
   "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
 
 typed_print_translation \<open>
- [(\<^const_syntax>\<open>Multiset.Ball\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBall\<close>),
-  (\<^const_syntax>\<open>Multiset.Bex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBex\<close>)]
+ [(\<^const_syntax>\<open>Multiset.Ball\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBall\<close>),
+  (\<^const_syntax>\<open>Multiset.Bex\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_MBex\<close>)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 lemma count_eq_zero_iff:

--- a/src/HOL/Probability/Probability_Measure.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -283,7 +283,7 @@
       end
     | unnest_tuples pat = pat
 
-    fun tr' [sig_alg, Const (\<^const_syntax>\<open>Collect\<close>, _) $ t] =
+    fun tr' ctxt [sig_alg, Const (\<^const_syntax>\<open>Collect\<close>, _) $ t] =
       let
         val bound_dummyT = Const (\<^syntax_const>\<open>_bound\<close>, dummyT)
 
@@ -300,7 +300,7 @@
             end
         | go pattern elem (Abs abs) =
             let
-              val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' abs
+              val (x as (_ $ tx), t) = Syntax_Trans.atomic_abs_tr' ctxt abs
             in
               go ((x, 0) :: pattern) (bound_dummyT $ tx :: elem) t
             end
@@ -313,7 +313,7 @@
         go [] [] t
       end
   in
-    [(\<^const_syntax>\<open>Sigma_Algebra.measure\<close>, K tr')]
+    [(\<^const_syntax>\<open>Sigma_Algebra.measure\<close>, tr')]
   end
 \<close>
 

--- a/src/HOL/Product_Type.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/Product_Type.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -315,34 +315,34 @@
 
 typed_print_translation \<open>
   let
-    fun case_prod_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match
-      | case_prod_guess_names_tr' T [Abs (x, xT, t)] =
+    fun case_prod_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
+      | case_prod_guess_names_tr' ctxt T [Abs (x, xT, t)] =
           (case (head_of t) of
             Const (\<^const_syntax>\<open>case_prod\<close>, _) => raise Match
           | _ =>
             let
               val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
-              val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0);
-              val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t');
+              val (y, t') = Syntax_Trans.atomic_abs_tr' ctxt ("y", yT, incr_boundvars 1 t $ Bound 0);
+              val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, xT, t');
             in
               Syntax.const \<^syntax_const>\<open>_abs\<close> $
                 (Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x' $ y) $ t''
             end)
-      | case_prod_guess_names_tr' T [t] =
+      | case_prod_guess_names_tr' ctxt T [t] =
           (case head_of t of
             Const (\<^const_syntax>\<open>case_prod\<close>, _) => raise Match
           | _ =>
             let
               val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
               val (y, t') =
-                Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
-              val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t');
+                Syntax_Trans.atomic_abs_tr' ctxt ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0);
+              val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt ("x", xT, t');
             in
               Syntax.const \<^syntax_const>\<open>_abs\<close> $
                 (Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x' $ y) $ t''
             end)
-      | case_prod_guess_names_tr' _ _ = raise Match;
-  in [(\<^const_syntax>\<open>case_prod\<close>, K case_prod_guess_names_tr')] end
+      | case_prod_guess_names_tr' _ _ _ = raise Match;
+  in [(\<^const_syntax>\<open>case_prod\<close>, case_prod_guess_names_tr')] end
 \<close>
 
 text \<open>Reconstruct pattern from (nested) \<^const>\<open>case_prod\<close>s,
@@ -351,39 +351,39 @@
 
 print_translation \<open>
   let
-    fun case_prod_tr' [Abs (x, T, t as (Abs abs))] =
+    fun case_prod_tr' ctxt [Abs (x, T, t as (Abs abs))] =
           (* case_prod (\<lambda>x y. t) \<Rightarrow> \<lambda>(x, y) t *)
           let
-            val (y, t') = Syntax_Trans.atomic_abs_tr' abs;
-            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
+            val (y, t') = Syntax_Trans.atomic_abs_tr' ctxt abs;
+            val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, t');
           in
             Syntax.const \<^syntax_const>\<open>_abs\<close> $
               (Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x' $ y) $ t''
           end
-      | case_prod_tr' [Abs (x, T, (s as Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t))] =
+      | case_prod_tr' ctxt [Abs (x, T, (s as Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t))] =
           (* case_prod (\<lambda>x. (case_prod (\<lambda>y z. t))) \<Rightarrow> \<lambda>(x, y, z). t *)
           let
             val Const (\<^syntax_const>\<open>_abs\<close>, _) $
               (Const (\<^syntax_const>\<open>_pattern\<close>, _) $ y $ z) $ t' =
-                case_prod_tr' [t];
-            val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t');
+                case_prod_tr' ctxt [t];
+            val (x', t'') = Syntax_Trans.atomic_abs_tr' ctxt (x, T, t');
           in
             Syntax.const \<^syntax_const>\<open>_abs\<close> $
               (Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x' $
                 (Syntax.const \<^syntax_const>\<open>_patterns\<close> $ y $ z)) $ t''
           end
-      | case_prod_tr' [Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t] =
+      | case_prod_tr' ctxt [Const (\<^const_syntax>\<open>case_prod\<close>, _) $ t] =
           (* case_prod (case_prod (\<lambda>x y z. t)) \<Rightarrow> \<lambda>((x, y), z). t *)
-          case_prod_tr' [(case_prod_tr' [t])]
+          case_prod_tr' ctxt [(case_prod_tr' ctxt [t])]
             (* inner case_prod_tr' creates next pattern *)
-      | case_prod_tr' [Const (\<^syntax_const>\<open>_abs\<close>, _) $ x_y $ Abs abs] =
+      | case_prod_tr' ctxt [Const (\<^syntax_const>\<open>_abs\<close>, _) $ x_y $ Abs abs] =
           (* case_prod (\<lambda>pttrn z. t) \<Rightarrow> \<lambda>(pttrn, z). t *)
-          let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in
+          let val (z, t) = Syntax_Trans.atomic_abs_tr' ctxt abs in
             Syntax.const \<^syntax_const>\<open>_abs\<close> $
               (Syntax.const \<^syntax_const>\<open>_pattern\<close> $ x_y $ z) $ t
           end
-      | case_prod_tr' _ = raise Match;
-  in [(\<^const_syntax>\<open>case_prod\<close>, K case_prod_tr')] end
+      | case_prod_tr' _ _ = raise Match;
+  in [(\<^const_syntax>\<open>case_prod\<close>, case_prod_tr')] end
 \<close>
 
 

--- a/src/HOL/Set.thy	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/HOL/Set.thy	Fri Dec 06 20:26:33 2024 +0100
@@ -324,8 +324,8 @@
 \<close>
 
 typed_print_translation \<open>
- [(\<^const_syntax>\<open>Ball\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Ball\<close>),
-  (\<^const_syntax>\<open>Bex\<close>, fn _ => Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Bex\<close>)]
+ [(\<^const_syntax>\<open>Ball\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Ball\<close>),
+  (\<^const_syntax>\<open>Bex\<close>, Syntax_Trans.preserve_binder_abs2_tr' \<^syntax_const>\<open>_Bex\<close>)]
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 print_translation \<open>
@@ -348,7 +348,7 @@
       if check (P, 0) then tr' P
       else
         let
-          val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' abs;
+          val (x as _ $ Free(xN, _), t) = Syntax_Trans.atomic_abs_tr' ctxt abs;
           val M = Syntax.const \<^syntax_const>\<open>_Coll\<close> $ x $ t;
         in
           case t of

--- a/src/Pure/Isar/subgoal.ML	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/Pure/Isar/subgoal.ML	Fri Dec 06 20:26:33 2024 +0100
@@ -171,7 +171,7 @@
     val subgoal = #1 (Logic.dest_implies (Thm.prop_of st));
     val subgoal_params =
       map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
-      |> Term.variant_bounds subgoal |> map #1;
+      |> Syntax_Trans.variant_bounds ctxt subgoal |> map #1;
 
     val n = length subgoal_params;
     val m = length raw_param_specs;

--- a/src/Pure/Syntax/syntax_phases.ML	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Dec 06 20:26:33 2024 +0100
@@ -735,13 +735,18 @@
 val typing_elem = YXML.output_markup_elem Markup.typing;
 val sorting_elem = YXML.output_markup_elem Markup.sorting;
 
-val exclude_consts =
+fun exclude_consts ast ctxt =
   let
-    fun exclude (Ast.Appl [Ast.Constant "_bound", Ast.Variable x]) = Symset.insert x
+    val s = the_default "" (Syntax_Trans.default_struct ctxt);
+
+    fun exclude (Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]) = Symset.insert s
+      | exclude (Ast.Constant c) =
+          if Lexicon.is_fixed c then Symset.insert (Lexicon.unmark_fixed c) else I
+      | exclude (Ast.Appl [Ast.Constant "_bound", Ast.Variable x]) = Symset.insert x
       | exclude (Ast.Appl [Ast.Constant "_free", Ast.Variable x]) = Symset.insert x
       | exclude (Ast.Appl asts) = fold exclude asts
       | exclude _ = I;
-  in Proof_Context.exclude_consts o Symset.build o exclude end;
+  in Proof_Context.exclude_consts (Symset.build (exclude ast)) ctxt end;
 
 fun unparse_t t_to_ast pretty_flags language_markup ctxt0 t =
   let

--- a/src/Pure/Syntax/syntax_trans.ML	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Fri Dec 06 20:26:33 2024 +0100
@@ -31,13 +31,14 @@
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val mark_bound_abs: string * typ -> term
   val mark_bound_body: string * typ -> term
-  val bound_vars: (string * typ) list -> term -> term
+  val variant_bounds: Proof.context -> term -> (string * 'a) list -> (string * 'a) list
+  val bound_vars: Proof.context -> (string * typ) list -> term -> term
   val abs_tr': Proof.context -> term -> term
-  val atomic_abs_tr': string * typ * term -> term * term
+  val atomic_abs_tr': Proof.context -> string * typ * term -> term * term
   val const_abs_tr': term -> term
   val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
-  val preserve_binder_abs_tr': string -> typ -> term list -> term
-  val preserve_binder_abs2_tr': string -> typ -> term list -> term
+  val preserve_binder_abs_tr': string -> Proof.context -> typ -> term list -> term
+  val preserve_binder_abs2_tr': string -> Proof.context -> typ -> term list -> term
   val print_abs: string * typ * term -> string * term
   val dependent_tr': string * string -> term list -> term
   val antiquote_tr': string -> term -> term
@@ -76,7 +77,6 @@
     (print_mode_value ()) <> SOME type_bracketsN;
 
 
-
 (** parse (ast) translations **)
 
 (* strip_positions *)
@@ -304,14 +304,27 @@
 fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);
 fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
 
-fun bound_vars vars body =
-  subst_bounds (map mark_bound_abs (rev (Term.variant_bounds body vars)), body);
+fun variant_bounds ctxt t =
+  let
+    val s = the_default "" (default_struct ctxt);
 
-fun strip_abss vars_of body_of tm =
+    fun declare (Const ("_struct", _) $ Const ("_indexdefault", _)) = Name.declare s
+      | declare (Const (c, _)) =
+          if Lexicon.is_fixed c then Name.declare (Lexicon.unmark_fixed c) else I
+      | declare (Free (x, _)) = Name.declare x
+      | declare (t $ u) = declare t #> declare u
+      | declare (Abs (_, _, t)) = declare t
+      | declare _ = I;
+  in Name.variant_names_build (declare t) end;
+
+fun bound_vars ctxt vars body =
+  subst_bounds (map mark_bound_abs (rev (variant_bounds ctxt body vars)), body);
+
+fun strip_abss ctxt vars_of body_of tm =
   let
     val vars = vars_of tm;
     val body = body_of tm;
-    val new_vars = Term.variant_bounds body vars;
+    val new_vars = variant_bounds ctxt body vars;
     fun subst (x, T) b =
       if Name.is_internal x andalso not (Term.is_dependent b)
       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
@@ -322,10 +335,10 @@
 
 fun abs_tr' ctxt tm =
   uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))
-    (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
+    (strip_abss ctxt strip_abs_vars strip_abs_body (eta_contr ctxt tm));
 
-fun atomic_abs_tr' (x, T, t) =
-  let val xT = singleton (Term.variant_bounds t) (x, T)
+fun atomic_abs_tr' ctxt (x, T, t) =
+  let val xT = singleton (variant_bounds ctxt t) (x, T)
   in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
 
 fun abs_ast_tr' asts =
@@ -349,21 +362,21 @@
       | mk_idts [idt] = idt
       | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts;
 
-    fun tr' t =
+    fun tr' ctxt t =
       let
-        val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
+        val (xs, bd) = strip_abss ctxt (strip_qnt_vars name) (strip_qnt_body name) t;
       in Syntax.const syn $ mk_idts xs $ bd end;
 
-    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
-      | binder_tr' [] = raise Match;
-  in (name, fn _ => binder_tr') end;
+    fun binder_tr' ctxt (t :: ts) = Term.list_comb (tr' ctxt (Syntax.const name $ t), ts)
+      | binder_tr' _ [] = raise Match;
+  in (name, binder_tr') end;
 
-fun preserve_binder_abs_tr' syn ty (Abs abs :: ts) =
-  let val (x, t) = atomic_abs_tr' abs
+fun preserve_binder_abs_tr' syn ctxt ty (Abs abs :: ts) =
+  let val (x, t) = atomic_abs_tr' ctxt abs
   in list_comb (Const (syn, ty) $ x $ t, ts) end;
 
-fun preserve_binder_abs2_tr' syn ty (A :: Abs abs :: ts) =
-  let val (x, t) = atomic_abs_tr' abs
+fun preserve_binder_abs2_tr' syn ctxt ty (A :: Abs abs :: ts) =
+  let val (x, t) = atomic_abs_tr' ctxt abs
   in list_comb (Const (syn, ty) $ x $ A $ t, ts) end;
 
 

--- a/src/Pure/primitive_defs.ML	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/Pure/primitive_defs.ML	Fri Dec 06 20:26:33 2024 +0100
@@ -31,7 +31,7 @@
     val eq_body = Term.strip_all_body eq;
 
     val display_terms =
-      commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
+      commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars ctxt eq_vars);
     val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
 
     val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";

--- a/src/Pure/type_infer_context.ML	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/Pure/type_infer_context.ML	Fri Dec 06 20:26:33 2024 +0100
@@ -248,7 +248,7 @@
         val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
         val (Ts', Ts'') = chop (length Ts) Ts_bTs';
         fun prep t =
-          let val xs = rev (Term.variant_bounds t (rev (map fst bs ~~ Ts'')))
+          let val xs = rev (Syntax_Trans.variant_bounds ctxt t (rev (map fst bs ~~ Ts'')))
           in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
       in (map prep ts', Ts') end;
 

--- a/src/Pure/variable.ML	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/Pure/variable.ML	Fri Dec 06 20:26:33 2024 +0100
@@ -705,7 +705,7 @@
 
 fun focus_params bindings t ctxt =
   let
-    val ps = Term.variant_bounds t (Term.strip_all_vars t);
+    val ps = Syntax_Trans.variant_bounds ctxt t (Term.strip_all_vars t);
     val (xs, Ts) = split_list ps;
     val (xs', ctxt') =
       (case bindings of

--- a/src/Tools/induct.ML	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/Tools/induct.ML	Fri Dec 06 20:26:33 2024 +0100
@@ -607,7 +607,7 @@
   let
     val maxidx = Thm.maxidx_of st;
     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
-    val params = Term.variant_bounds goal (Logic.strip_params goal);
+    val params = Syntax_Trans.variant_bounds ctxt goal (Logic.strip_params goal);
   in
     if not (null params) then
       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^

--- a/src/Tools/subtyping.ML	Fri Dec 06 15:20:43 2024 +0100
+++ b/src/Tools/subtyping.ML	Fri Dec 06 20:26:33 2024 +0100
@@ -244,7 +244,7 @@
     val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
     val (Ts', Ts'') = chop (length Ts) Ts_bTs';
     fun prep t =
-      let val xs = rev (Term.variant_bounds t (rev (map fst bs ~~ Ts'')))
+      let val xs = rev (Syntax_Trans.variant_bounds ctxt t (rev (map fst bs ~~ Ts'')))
       in Term.subst_bounds (map Syntax_Trans.mark_bound_abs xs, t) end;
   in (map prep ts', Ts') end;