diff -r f012cbfd96d0 -r cdc43c0fdbfc src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Nov 30 22:02:36 2024 +0100
+++ b/src/Pure/variable.ML	Sat Nov 30 22:33:21 2024 +0100
@@ -17,13 +17,13 @@
   val def_sort: Proof.context -> indexname -> sort option
   val declare_maxidx: int -> Proof.context -> Proof.context
   val declare_names: term -> Proof.context -> Proof.context
+  val variant_names: Proof.context -> (string * 'a) list -> (string * 'a) list
   val declare_constraints: term -> Proof.context -> Proof.context
   val declare_internal: term -> Proof.context -> Proof.context
   val declare_term: term -> Proof.context -> Proof.context
   val declare_typ: typ -> Proof.context -> Proof.context
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
   val declare_thm: thm -> Proof.context -> Proof.context
-  val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
   val bind_term: indexname * term -> Proof.context -> Proof.context
   val unbind_term: indexname -> Proof.context -> Proof.context
   val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
@@ -211,7 +211,7 @@
 val declare_maxidx = map_maxidx o Integer.max;
 
 
-(* names *)
+(* type/term names *)
 
 fun declare_type_names t =
   map_names (Term.declare_tfree_names t) #>
@@ -222,6 +222,8 @@
   map_names (Term.declare_free_names t) #>
   map_maxidx (Term.maxidx_term t);
 
+fun variant_names ctxt xs = Name.variant_names (names_of ctxt) xs;
+
 
 (* type occurrences *)
 
@@ -275,12 +277,6 @@
 val declare_thm = Thm.fold_terms {hyps = true} declare_internal;
 
 
-(* renaming term/type frees *)
-
-fun variant_frees ctxt ts frees =
-  Name.variant_names (names_of (fold declare_names ts ctxt)) frees;
-
-
 
 (** term bindings **)