1.1 --- a/src/Pure/proofterm.ML	Fri Aug 19 18:01:23 2011 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Fri Aug 19 21:40:52 2011 +0200
     1.3 @@ -37,11 +37,11 @@
     1.4  
     1.5    type oracle = string * term
     1.6    type pthm = serial * (string * term * proof_body future)
     1.7 +  val join_body: proof_body -> unit
     1.8    val proof_of: proof_body -> proof
     1.9    val join_proof: proof_body future -> proof
    1.10    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    1.11    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
    1.12 -  val join_bodies: proof_body list -> unit
    1.13    val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    1.14  
    1.15    val oracle_ord: oracle * oracle -> order
    1.16 @@ -171,6 +171,10 @@
    1.17  type oracle = string * term;
    1.18  type pthm = serial * (string * term * proof_body future);
    1.19  
    1.20 +fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
    1.21 +fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
    1.22 +fun join_body (PBody {thms, ...}) = join_thms thms;
    1.23 +
    1.24  fun proof_of (PBody {proof, ...}) = proof;
    1.25  val join_proof = Future.join #> proof_of;
    1.26  
    1.27 @@ -195,18 +199,15 @@
    1.28  fun fold_body_thms f =
    1.29    let
    1.30      fun app (PBody {thms, ...}) =
    1.31 -     (Future.join_results (map (#3 o #2) thms);
    1.32 -      thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    1.33 +      tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    1.34          if Inttab.defined seen i then (x, seen)
    1.35          else
    1.36            let
    1.37              val body' = Future.join body;
    1.38              val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    1.39 -          in (f (name, prop, body') x', seen') end));
    1.40 +          in (f (name, prop, body') x', seen') end);
    1.41    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    1.42  
    1.43 -fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    1.44 -
    1.45  fun status_of bodies =
    1.46    let
    1.47      fun status (PBody {oracles, thms, ...}) x =
    1.48 @@ -242,14 +243,13 @@
    1.49  val all_oracles_of =
    1.50    let
    1.51      fun collect (PBody {oracles, thms, ...}) =
    1.52 -     (Future.join_results (map (#3 o #2) thms);
    1.53 -      thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
    1.54 +      tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) =>
    1.55          if Inttab.defined seen i then (x, seen)
    1.56          else
    1.57            let
    1.58              val body' = Future.join body;
    1.59              val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
    1.60 -          in (merge_oracles oracles x', seen') end));
    1.61 +          in (merge_oracles oracles x', seen') end);
    1.62    in fn body => #1 (collect body ([], Inttab.empty)) end;
    1.63  
    1.64  fun approximate_proof_body prf =
    1.65 @@ -1396,6 +1396,7 @@
    1.66        | fill _ = NONE;
    1.67      val (rules, procs) = get_data thy;
    1.68      val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
    1.69 +    val _ = join_thms thms;
    1.70    in PBody {oracles = oracles, thms = thms, proof = proof} end;
    1.71  
    1.72  fun fulfill_proof_future _ [] postproc body =

     2.1 --- a/src/Pure/thm.ML	Fri Aug 19 18:01:23 2011 +0200
     2.2 +++ b/src/Pure/thm.ML	Fri Aug 19 21:40:52 2011 +0200
     2.3 @@ -517,9 +517,9 @@
     2.4      (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
     2.5  and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
     2.6  
     2.7 -val join_proofs = Proofterm.join_bodies o map fulfill_body;
     2.8 +fun join_proofs thms = ignore (map fulfill_body thms);
     2.9  
    2.10 -fun proof_body_of thm = (Proofterm.join_bodies [raw_body thm]; fulfill_body thm);
    2.11 +fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
    2.12  val proof_of = Proofterm.proof_of o proof_body_of;
    2.13  
    2.14