clarified modules (see also e063c0403650);

--- a/src/Pure/name.ML	Sat Jul 20 19:30:03 2024 +0200
+++ b/src/Pure/name.ML	Sat Jul 20 21:17:22 2024 +0200
@@ -31,6 +31,7 @@
   val invent_names: context -> string -> 'a list -> (string * 'a) list
   val invent_list: string list -> string -> int -> string list
   val variant: string -> context -> string * context
+  val variant_bound: string -> context -> string * context
   val variant_list: string list -> string list -> string list
   val enforce_case: bool -> string -> string
   val desymbolize: bool option -> string -> string
@@ -150,6 +151,8 @@
         in (x', ctxt') end;
   in (x' ^ replicate_string n "_", ctxt') end;
 
+fun variant_bound name = variant (if is_bound name then "u" else name);
+
 fun variant_list used names = #1 (make_context used |> fold_map variant names);
 
 

--- a/src/Pure/term_subst.ML	Sat Jul 20 19:30:03 2024 +0200
+++ b/src/Pure/term_subst.ML	Sat Jul 20 21:17:22 2024 +0200
@@ -230,7 +230,7 @@
 (* zero var indexes *)
 
 fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) =
-  let val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used
+  let val (x', used') = Name.variant_bound x used
   in if x = x' andalso i = 0 then (inst, used') else (ins (v, mk ((x', 0), X)) inst, used') end;
 
 fun zero_var_indexes_inst used ts =