src/Pure/thm.ML

--- a/src/Pure/thm.ML	Sat Aug 20 15:52:29 2011 +0200
+++ b/src/Pure/thm.ML	Sat Aug 20 16:06:27 2011 +0200
@@ -95,9 +95,10 @@
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
-  val join_proofs: thm list -> unit
+  val future_body_of: thm -> proof_body future
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
+  val join_proofs: thm list -> unit
   val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_name: thm -> string
@@ -510,17 +511,23 @@
 
 (* fulfilled proofs *)
 
-fun raw_body (Thm (Deriv {body, ...}, _)) = body;
+fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
+fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
+
+fun join_promises [] = ()
+  | join_promises promises = join_promises_of (Future.joins (map snd promises))
+and join_promises_of thms = join_promises (maps raw_promises_of thms);
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
-    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
-and fulfill_bodies futures = map fulfill_body (Future.joins futures);
+  Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body
+and fulfill_promises promises =
+  map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
 
-fun join_proofs thms = ignore (map fulfill_body thms);
+val future_body_of = Proofterm.check_body_thms o fulfill_body;
+val proof_body_of = Future.join o future_body_of;
+val proof_of = Proofterm.proof_of o proof_body_of;
 
-fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
-val proof_of = Proofterm.proof_of o proof_body_of;
+fun join_proofs thms = (join_promises_of thms; Future.joins (map future_body_of thms); ());
 
 
 (* derivation status *)
@@ -529,7 +536,7 @@
   let
     val ps = map (Future.peek o snd) promises;
     val bodies = body ::
-      map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
+      map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
     val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   in
    {oracle = oracle,
@@ -552,7 +559,7 @@
     val _ = null hyps orelse err "bad hyps";
     val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
     val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
-    val _ = fulfill_bodies (map #2 promises);
+    val _ = join_promises promises;
   in thm end;
 
 fun future future_thm ct =