--- a/src/Pure/term.ML Thu Jan 17 21:03:29 2002 +0100
+++ b/src/Pure/term.ML Thu Jan 17 21:03:55 2002 +0100
@@ -155,6 +155,7 @@
val add_term_consts: term * string list -> string list
val add_term_frees: term * term list -> term list
val term_frees: term -> term list
+ val add_term_free_names: term * string list -> string list
val add_term_names: term * string list -> string list
val add_term_tfree_names: term * string list -> string list
val add_term_tfrees: term * (string * sort) list -> (string * sort) list
@@ -804,6 +805,12 @@
(*maps (bs,v) to v'::bs this reverses the identifiers bs*)
fun add_new_id (bs, c) : string list = variant bs c :: bs;
+(*Accumulates the names of Frees in the term, suppressing duplicates.*)
+fun add_term_free_names (Free(a,_), bs) = a ins_string 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) = NameSpace.base a ins_string bs