diff -r 44c0028486db -r 31b05aef022d src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/term.ML	Sat Nov 30 19:21:38 2024 +0100
@@ -166,7 +166,6 @@
   val strip_sortsT_same: typ Same.operation
   val strip_sortsT: typ -> typ
   val strip_sorts: term -> term
-  val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   val eq_ix: indexname * indexname -> bool
   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   val eq_var: (indexname * typ) * (indexname * typ) -> bool
@@ -607,8 +606,6 @@
   #1 (fold_map Name.variant (map fst frees) (Name.build_context (declare_term_names t))) ~~
     map #2 frees;
 
-fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
-
 
 (* sorts *)