# HG changeset patch
# User wenzelm
# Date 1733522829 -3600
# Node ID ee07998f9b259ea98501dd9d3ea62e2b5ce6a999
# Parent  6e350220dcd1597381c745ae210216efc55006da
obsolete;

diff -r 6e350220dcd1 -r ee07998f9b25 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Dec 06 22:40:43 2024 +0100
+++ b/src/Pure/term.ML	Fri Dec 06 23:07:09 2024 +0100
@@ -159,8 +159,6 @@
   val declare_var_names: (int -> bool) -> term -> Name.context -> Name.context
   val variant_bounds: term -> (string * 'a) list -> (string * 'a) list
   val hidden_polymorphism: term -> (indexname * sort) list
-  val declare_term_names: term -> Name.context -> Name.context
-  val variant_frees: term -> (string * 'a) list -> (string * 'a) list
   val smash_sortsT_same: sort -> typ Same.operation
   val smash_sortsT: sort -> typ -> typ
   val smash_sorts: sort -> term -> term
@@ -577,13 +575,14 @@
 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
 val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
 val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
+
+(*renaming variables*)
 val declare_tfree_namesT = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
 val declare_tfree_names = fold_types declare_tfree_namesT;
 fun declare_tvar_namesT pred = fold_atyps (fn TVar ((a, i), _) => pred i ? Name.declare a | _ => I);
 val declare_tvar_names = fold_types o declare_tvar_namesT;
 val declare_free_names = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
 fun declare_var_names pred = fold_aterms (fn Var ((x, i), _) => pred i ? Name.declare x | _ => I);
-
 fun variant_bounds t = Name.variant_names_build (declare_free_names t);
 
 (*extra type variables in a term, not covered by its type*)
@@ -596,19 +595,6 @@
   in extra_tvars end;
 
 
-(* renaming variables *)
-
-fun declare_term_names tm =
-  fold_aterms
-    (fn Const (a, _) => Name.declare (Long_Name.base_name a)
-      | Free (a, _) => Name.declare a
-      | _ => I) tm #>
-  declare_tfree_names tm;
-
-fun variant_frees t frees =
-  Name.variant_names_build (declare_term_names t) frees;
-
-
 (* sorts *)
 
 fun smash_sortsT_same S' =