# HG changeset patch
# User wenzelm
# Date 1131652639 -3600
# Node ID c6899e23b5ff45e6af802536dd009738a705950f
# Parent  7921f41165cf4ff717726f12209241919db3ba52
added find_free (from Isar/proof_context.ML);

diff -r 7921f41165cf -r c6899e23b5ff src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Nov 10 20:57:18 2005 +0100
+++ b/src/Pure/term.ML	Thu Nov 10 20:57:19 2005 +0100
@@ -75,6 +75,7 @@
   val add_term_names: term * string list -> string list
   val add_term_varnames: term -> indexname list -> indexname list
   val term_varnames: term -> indexname list
+  val find_free: term -> string -> term option
   val aconv: term * term -> bool
   val aconvs: term list * term list -> bool
   structure Vartab: TABLE
@@ -500,6 +501,14 @@
 val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
 fun term_varnames t = add_term_varnames t [];
 
+fun find_free t x =
+  let
+    exception Found of term;
+    fun find (t as Free (x', _)) = if x = x' then raise Found t else I
+      | find _ = I;
+  in (fold_aterms find t (); NONE) handle Found v => SOME v end;
+
+
 
 (** Comparing terms, types, sorts etc. **)