--- 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 *)