# HG changeset patch
# User wenzelm
# Date 1153855088 -7200
# Node ID 24b49cbd438b8f82c97962d930f887cc18bf908a
# Parent  c6fb50dbbc304c555425d28fb84305b693be6a11
added find_free (from term.ML);

diff -r c6fb50dbbc30 -r 24b49cbd438b src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Jul 25 21:18:07 2006 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jul 25 21:18:08 2006 +0200
@@ -99,6 +99,13 @@
 
 local
 
+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;
+
 fun gen_obtain prep_att prep_vars prep_propp
     name raw_vars raw_asms int state =
   let
@@ -124,7 +131,7 @@
     val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
 
     fun occs_var x = Library.get_first (fn t =>
-      Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
+      find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
     val parms =
       map_filter (fn (SOME (Free a), x) => SOME (a, x) | _ => NONE) (map occs_var xs ~~ xs);