# HG changeset patch
# User wenzelm
# Date 1313860863 -7200
# Node ID cc53ce50f738f59865cdf49769140b8fa05322a3
# Parent  e10f6b873f88d2d5740abe343772291f2f6c1f13
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOL-Proofs) -- see also aa9c1e9ef2ce and 4e2abb045eac;

diff -r e10f6b873f88 -r cc53ce50f738 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sat Aug 20 18:11:17 2011 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 20 19:21:03 2011 +0200
@@ -40,7 +40,7 @@
                path = "",
                parents = parents};
           in cons entry end;
-    val deps = Proofterm.fold_body_thms add_dep (Future.joins (map Thm.future_body_of thms)) [];
+    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
   in Present.display_graph (sort_wrt #ID deps) end;
 
 
@@ -66,7 +66,7 @@
     val used =
       Proofterm.fold_body_thms
         (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
-        (map Proofterm.strip_thm (Future.joins (map (Thm.future_body_of o #1 o #2) new_thms)))
+        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
         Symtab.empty;
 
     fun is_unused a = not (Symtab.defined used a);
diff -r e10f6b873f88 -r cc53ce50f738 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Aug 20 18:11:17 2011 +0200
+++ b/src/Pure/proofterm.ML	Sat Aug 20 19:21:03 2011 +0200
@@ -37,11 +37,11 @@
 
   type oracle = string * term
   type pthm = serial * (string * term * proof_body future)
-  val check_body_thms: proof_body -> proof_body future
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
+  val join_bodies: proof_body list -> unit
   val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
@@ -171,17 +171,11 @@
 type oracle = string * term;
 type pthm = serial * (string * term * proof_body future);
 
-fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
-
-fun check_body_thms (body as PBody {thms, ...}) =
-  (singleton o Future.cond_forks)
-    {name = "Proofterm.check_body_thms", group = NONE,
-      deps = map (Future.task_of o #3 o #2) thms, pri = 0, interrupts = true}
-    (fn () => (join_thms thms; body));
-
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
 
+fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
+
 
 (***** proof atoms *****)
 
@@ -212,6 +206,8 @@
           in (f (name, prop, body') x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
+fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
+
 fun status_of bodies =
   let
     fun status (PBody {oracles, thms, ...}) x =
@@ -1467,13 +1463,7 @@
             deps = [], pri = 0, interrupts = true}
           (make_body0 o full_proof0);
 
-    fun new_prf () =
-      let
-        val body' = body0
-          |> fulfill_proof_future thy promises postproc
-          |> Future.map (fn body as PBody {thms, ...} => (join_thms thms; body));
-      in (serial (), body') end;
-
+    fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)
       (case strip_combt (fst (strip_combP prf)) of
diff -r e10f6b873f88 -r cc53ce50f738 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 20 18:11:17 2011 +0200
+++ b/src/Pure/thm.ML	Sat Aug 20 19:21:03 2011 +0200
@@ -95,7 +95,7 @@
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
-  val future_body_of: thm -> proof_body future
+  val proof_bodies_of: thm list -> proof_body list
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
   val join_proofs: thm list -> unit
@@ -523,11 +523,17 @@
 and fulfill_promises promises =
   map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
 
-val future_body_of = Proofterm.check_body_thms o fulfill_body;
-val proof_body_of = Future.join o future_body_of;
+fun proof_bodies_of thms =
+  let
+    val _ = join_promises_of thms;
+    val bodies = map fulfill_body thms;
+    val _ = Proofterm.join_bodies bodies;
+  in bodies end;
+
+val proof_body_of = singleton proof_bodies_of;
 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); ());
+val join_proofs = ignore o proof_bodies_of;
 
 
 (* derivation status *)