src/Pure/term.ML
changeset 15025 b2ef0bc6f59f
parent 14854 61bdf2ae4dc5
child 15472 4674102737e9
     1.1 --- a/src/Pure/term.ML	Thu Jul 08 19:34:00 2004 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Jul 08 19:34:10 2004 +0200
     1.3 @@ -75,6 +75,8 @@
     1.4    val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
     1.5    val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
     1.6    val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term
     1.7 +  val add_term_varnames: indexname list * term -> indexname list
     1.8 +  val term_varnames: term -> indexname list
     1.9    val dummyT: typ
    1.10    val itselfT: typ -> typ
    1.11    val a_itselfT: typ
    1.12 @@ -944,6 +946,9 @@
    1.13  val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
    1.14  val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
    1.15  
    1.16 +(*collect variable names*)
    1.17 +val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
    1.18 +fun term_varnames t = add_term_varnames ([], t);
    1.19  
    1.20  
    1.21  (** type and term orders **)