ProofContext.find_free;
authorwenzelm
Thu Mar 30 14:24:46 2000 +0200 (2000-03-30)
changeset 861430cc975727f1
parent 8613 ec9ba98587a9
child 8615 419166fa66d0
ProofContext.find_free;
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/obtain.ML	Thu Mar 30 14:22:15 2000 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Thu Mar 30 14:24:46 2000 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4  
     1.5      (*that_prop*)
     1.6      fun find_free x t =
     1.7 -      (case Proof.find_free t x of Some (Free a) => Some a | _ => None);
     1.8 +      (case ProofContext.find_free t x of Some (Free a) => Some a | _ => None);
     1.9      fun occs_var x = Library.get_first (find_free x) asm_props;
    1.10      val that_prop =
    1.11        Term.list_all_free (mapfilter occs_var xs, Logic.list_implies (asm_props, atomic_thesis));