# HG changeset patch
# User wenzelm
# Date 1237996457 -3600
# Node ID 465093aa58449453da9a480616d22ee9fa633f4f
# Parent  2ee706293eb589a7bd855b9d19475ca99780db54
fulfill_proof/thm_proof: pass whole proof_body, not just the projection to proof (which might be incomplete);
more explicit oracle_proof;

diff -r 2ee706293eb5 -r 465093aa5844 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Mar 25 16:52:50 2009 +0100
+++ b/src/Pure/thm.ML	Wed Mar 25 16:54:17 2009 +0100
@@ -1662,7 +1662,7 @@
 fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
   let
     val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
-    val ps = map (apsnd (raw_proof_of o Future.join)) promises;
+    val ps = map (apsnd (raw_proof_body_of o Future.join)) promises;
   in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
 
 val proof_of = Proofterm.proof_of o proof_body_of;
@@ -1680,7 +1680,7 @@
     val {thy_ref, hyps, prop, tpairs, ...} = args;
     val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
 
-    val ps = map (apsnd (Future.map proof_of)) promises;
+    val ps = map (apsnd (Future.map proof_body_of)) promises;
     val thy = Theory.deref thy_ref;
     val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
 
@@ -1701,8 +1701,8 @@
     if T <> propT then
       raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
     else
-      let val prf = Pt.oracle_proof name prop in
-        Thm (make_deriv ~1 [] [] (Pt.make_oracles prf) [] prf,
+      let val (ora, prf) = Pt.oracle_proof name prop in
+        Thm (make_deriv ~1 [] [] [ora] [] prf,
          {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
           tags = [],
           maxidx = maxidx,