# HG changeset patch
# User wenzelm
# Date 1230753540 -3600
# Node ID 40a1014cefaa20bb5fbffec2472c756f7135fd2e
# Parent  b22ccb3998db5ca09809d1f5a3bfe8df418ae1df
removed unused add_term_free_names;

diff -r b22ccb3998db -r 40a1014cefaa src/Pure/old_term.ML
--- a/src/Pure/old_term.ML	Wed Dec 31 20:31:36 2008 +0100
+++ b/src/Pure/old_term.ML	Wed Dec 31 20:59:00 2008 +0100
@@ -7,7 +7,6 @@
 signature OLD_TERM =
 sig
   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
-  val add_term_free_names: term * string list -> string list
   val add_term_names: term * string list -> string list
   val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
   val add_typ_tfree_names: typ * string list -> string list
@@ -40,12 +39,6 @@
       | iter(Bound _, a) = a
 in iter end
 
-(*Accumulates the names of Frees in the term, suppressing duplicates.*)
-fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
-  | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
-  | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
-  | add_term_free_names (_, bs) = bs;
-
 (*Accumulates the names in the term, suppressing duplicates.
   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
 fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs