# HG changeset patch
# User wenzelm
# Date 1089308050 -7200
# Node ID b2ef0bc6f59f673860825961329917bd0f433aa2
# Parent  341cd221c3e1f8a4e2e36132564f814243858e12
added add_term_varnames, term_varnames;

diff -r 341cd221c3e1 -r b2ef0bc6f59f src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Jul 08 19:34:00 2004 +0200
+++ b/src/Pure/term.ML	Thu Jul 08 19:34:10 2004 +0200
@@ -75,6 +75,8 @@
   val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
   val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
   val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
+  val add_term_varnames: indexname list * term -> indexname list
+  val term_varnames: term -> indexname list
   val dummyT: typ
   val itselfT: typ -> typ
   val a_itselfT: typ
@@ -944,6 +946,9 @@
 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
 val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
 
+(*collect variable names*)
+val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
+fun term_varnames t = add_term_varnames ([], t);
 
 
 (** type and term orders **)