# HG changeset patch
# User wenzelm
# Date 954419086 -7200
# Node ID 30cc975727f16f67b736772ad3b5071b12bacec7
# Parent  ec9ba98587a9438070b9507102c3490bf201c756
ProofContext.find_free;

diff -r ec9ba98587a9 -r 30cc975727f1 src/Pure/Isar/obtain.ML
--- 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));