src/Pure/term.ML
changeset 18149 c6899e23b5ff
parent 18131 8c3089df74ba
child 18183 a9f67248996a
     1.1 --- a/src/Pure/term.ML	Thu Nov 10 20:57:18 2005 +0100
     1.2 +++ b/src/Pure/term.ML	Thu Nov 10 20:57:19 2005 +0100
     1.3 @@ -75,6 +75,7 @@
     1.4    val add_term_names: term * string list -> string list
     1.5    val add_term_varnames: term -> indexname list -> indexname list
     1.6    val term_varnames: term -> indexname list
     1.7 +  val find_free: term -> string -> term option
     1.8    val aconv: term * term -> bool
     1.9    val aconvs: term list * term list -> bool
    1.10    structure Vartab: TABLE
    1.11 @@ -500,6 +501,14 @@
    1.12  val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
    1.13  fun term_varnames t = add_term_varnames t [];
    1.14  
    1.15 +fun find_free t x =
    1.16 +  let
    1.17 +    exception Found of term;
    1.18 +    fun find (t as Free (x', _)) = if x = x' then raise Found t else I
    1.19 +      | find _ = I;
    1.20 +  in (fold_aterms find t (); NONE) handle Found v => SOME v end;
    1.21 +
    1.22 +
    1.23  
    1.24  (** Comparing terms, types, sorts etc. **)
    1.25