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