src/Pure/Syntax/syntax_trans.ML

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