1.1 --- a/src/Pure/Thy/thm_deps.ML	Sat Aug 20 18:11:17 2011 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 20 19:21:03 2011 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4                 path = "",
     1.5                 parents = parents};
     1.6            in cons entry end;
     1.7 -    val deps = Proofterm.fold_body_thms add_dep (Future.joins (map Thm.future_body_of thms)) [];
     1.8 +    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
     1.9    in Present.display_graph (sort_wrt #ID deps) end;
    1.10  
    1.11  
    1.12 @@ -66,7 +66,7 @@
    1.13      val used =
    1.14        Proofterm.fold_body_thms
    1.15          (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
    1.16 -        (map Proofterm.strip_thm (Future.joins (map (Thm.future_body_of o #1 o #2) new_thms)))
    1.17 +        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
    1.18          Symtab.empty;
    1.19  
    1.20      fun is_unused a = not (Symtab.defined used a);

     2.1 --- a/src/Pure/proofterm.ML	Sat Aug 20 18:11:17 2011 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Sat Aug 20 19:21:03 2011 +0200
     2.3 @@ -37,11 +37,11 @@
     2.4  
     2.5    type oracle = string * term
     2.6    type pthm = serial * (string * term * proof_body future)
     2.7 -  val check_body_thms: proof_body -> proof_body future
     2.8    val proof_of: proof_body -> proof
     2.9    val join_proof: proof_body future -> proof
    2.10    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    2.11    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
    2.12 +  val join_bodies: proof_body list -> unit
    2.13    val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    2.14  
    2.15    val oracle_ord: oracle * oracle -> order
    2.16 @@ -171,17 +171,11 @@
    2.17  type oracle = string * term;
    2.18  type pthm = serial * (string * term * proof_body future);
    2.19  
    2.20 -fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
    2.21 -
    2.22 -fun check_body_thms (body as PBody {thms, ...}) =
    2.23 -  (singleton o Future.cond_forks)
    2.24 -    {name = "Proofterm.check_body_thms", group = NONE,
    2.25 -      deps = map (Future.task_of o #3 o #2) thms, pri = 0, interrupts = true}
    2.26 -    (fn () => (join_thms thms; body));
    2.27 -
    2.28  fun proof_of (PBody {proof, ...}) = proof;
    2.29  val join_proof = Future.join #> proof_of;
    2.30  
    2.31 +fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
    2.32 +
    2.33  
    2.34  (***** proof atoms *****)
    2.35  
    2.36 @@ -212,6 +206,8 @@
    2.37            in (f (name, prop, body') x', seen') end);
    2.38    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    2.39  
    2.40 +fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    2.41 +
    2.42  fun status_of bodies =
    2.43    let
    2.44      fun status (PBody {oracles, thms, ...}) x =
    2.45 @@ -1467,13 +1463,7 @@
    2.46              deps = [], pri = 0, interrupts = true}
    2.47            (make_body0 o full_proof0);
    2.48  
    2.49 -    fun new_prf () =
    2.50 -      let
    2.51 -        val body' = body0
    2.52 -          |> fulfill_proof_future thy promises postproc
    2.53 -          |> Future.map (fn body as PBody {thms, ...} => (join_thms thms; body));
    2.54 -      in (serial (), body') end;
    2.55 -
    2.56 +    fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    2.57      val (i, body') =
    2.58        (*non-deterministic, depends on unknown promises*)
    2.59        (case strip_combt (fst (strip_combP prf)) of

     3.1 --- a/src/Pure/thm.ML	Sat Aug 20 18:11:17 2011 +0200
     3.2 +++ b/src/Pure/thm.ML	Sat Aug 20 19:21:03 2011 +0200
     3.3 @@ -95,7 +95,7 @@
     3.4    val weaken: cterm -> thm -> thm
     3.5    val weaken_sorts: sort list -> cterm -> cterm
     3.6    val extra_shyps: thm -> sort list
     3.7 -  val future_body_of: thm -> proof_body future
     3.8 +  val proof_bodies_of: thm list -> proof_body list
     3.9    val proof_body_of: thm -> proof_body
    3.10    val proof_of: thm -> proof
    3.11    val join_proofs: thm list -> unit
    3.12 @@ -523,11 +523,17 @@
    3.13  and fulfill_promises promises =
    3.14    map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
    3.15  
    3.16 -val future_body_of = Proofterm.check_body_thms o fulfill_body;
    3.17 -val proof_body_of = Future.join o future_body_of;
    3.18 +fun proof_bodies_of thms =
    3.19 +  let
    3.20 +    val _ = join_promises_of thms;
    3.21 +    val bodies = map fulfill_body thms;
    3.22 +    val _ = Proofterm.join_bodies bodies;
    3.23 +  in bodies end;
    3.24 +
    3.25 +val proof_body_of = singleton proof_bodies_of;
    3.26  val proof_of = Proofterm.proof_of o proof_body_of;
    3.27  
    3.28 -fun join_proofs thms = (join_promises_of thms; Future.joins (map future_body_of thms); ());
    3.29 +val join_proofs = ignore o proof_bodies_of;
    3.30  
    3.31  
    3.32  (* derivation status *)