# HG changeset patch
# User wenzelm
# Date 1011297835 -3600
# Node ID c69bd9754473b3dac6e26e2e6e2d86152f6e77e6
# Parent  a94cef8982cc3a3582dae5b4dd733631e19c0816
added add_term_free_names (more precise/efficient than add_term_names);

diff -r a94cef8982cc -r c69bd9754473 src/Pure/term.ML
--- 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