# HG changeset patch
# User wenzelm
# Date 1248201452 -7200
# Node ID d1d98a02473ed7509594a1b862324bfaaa4960a5
# Parent  ebdcff2b9810bf2468e1c3c03daed277e045fdec
simultaneous join_proofs;
removed obsolete promises_of;

diff -r ebdcff2b9810 -r d1d98a02473e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jul 21 20:37:31 2009 +0200
+++ b/src/Pure/thm.ML	Tue Jul 21 20:37:32 2009 +0200
@@ -141,10 +141,9 @@
   val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   val rename_boundvars: term -> term -> thm -> thm
+  val join_proofs: thm list -> unit
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
-  val join_proof: thm -> unit
-  val promises_of: thm -> (serial * thm future) list
   val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val get_name: thm -> string
@@ -1616,15 +1615,14 @@
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
 and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
 
+val join_proofs = Pt.join_bodies o map fulfill_body;
+
 fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
 val proof_of = Pt.proof_of o proof_body_of;
-val join_proof = ignore o proof_body_of;
 
 
 (* derivation status *)
 
-fun promises_of (Thm (Deriv {promises, ...}, _)) = promises;
-
 fun status_of (Thm (Deriv {promises, body}, _)) =
   let
     val ps = map (Future.peek o snd) promises;
@@ -1744,5 +1742,5 @@
 
 end;
 
-structure BasicThm: BASIC_THM = Thm;
-open BasicThm;
+structure Basic_Thm: BASIC_THM = Thm;
+open Basic_Thm;