1.1 --- a/src/Pure/thm.ML	Tue Jul 21 20:37:31 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Jul 21 20:37:32 2009 +0200
     1.3 @@ -141,10 +141,9 @@
     1.4    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
     1.5    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
     1.6    val rename_boundvars: term -> term -> thm -> thm
     1.7 +  val join_proofs: thm list -> unit
     1.8    val proof_body_of: thm -> proof_body
     1.9    val proof_of: thm -> proof
    1.10 -  val join_proof: thm -> unit
    1.11 -  val promises_of: thm -> (serial * thm future) list
    1.12    val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
    1.13    val future: thm future -> cterm -> thm
    1.14    val get_name: thm -> string
    1.15 @@ -1616,15 +1615,14 @@
    1.16      (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
    1.17  and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
    1.18  
    1.19 +val join_proofs = Pt.join_bodies o map fulfill_body;
    1.20 +
    1.21  fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
    1.22  val proof_of = Pt.proof_of o proof_body_of;
    1.23 -val join_proof = ignore o proof_body_of;
    1.24  
    1.25  
    1.26  (* derivation status *)
    1.27  
    1.28 -fun promises_of (Thm (Deriv {promises, ...}, _)) = promises;
    1.29 -
    1.30  fun status_of (Thm (Deriv {promises, body}, _)) =
    1.31    let
    1.32      val ps = map (Future.peek o snd) promises;
    1.33 @@ -1744,5 +1742,5 @@
    1.34  
    1.35  end;
    1.36  
    1.37 -structure BasicThm: BASIC_THM = Thm;
    1.38 -open BasicThm;
    1.39 +structure Basic_Thm: BASIC_THM = Thm;
    1.40 +open Basic_Thm;