ProofContext.find_free;

--- a/src/Pure/Isar/obtain.ML	Thu Mar 30 14:22:15 2000 +0200
+++ b/src/Pure/Isar/obtain.ML	Thu Mar 30 14:24:46 2000 +0200
@@ -101,7 +101,7 @@
 
     (*that_prop*)
     fun find_free x t =
-      (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
+      (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
     fun occs_var x = Library.get_first (find_free x) asm_props;
     val that_prop =
       Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis));