# HG changeset patch
# User wenzelm
# Date 1524586208 -7200
# Node ID 0a6d6ba383dc1d1a3520437b0bd5411dd89317bc
# Parent  df9044efd0549860647c7eac228e2f8e5a595ea8
more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;

diff -r df9044efd054 -r 0a6d6ba383dc src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Apr 24 16:59:40 2018 +0200
+++ b/src/Pure/proofterm.ML	Tue Apr 24 18:10:08 2018 +0200
@@ -1610,16 +1610,14 @@
     val argsP = map OfClass outer_constraints @ map Hyp hyps;
 
     fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
-    fun make_body () =
-      make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
     val body0 =
       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
-      else if not (Multithreading.parallel_proofs_enabled 1) then Future.value (make_body ())
       else
         (singleton o Future.cond_forks)
           {name = "Proofterm.prepare_thm_proof", group = NONE,
-            deps = [], pri = 0, interrupts = true}
-          make_body;
+            deps = [], pri = 1, interrupts = true}
+          (fn () =>
+            make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf))));
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
     val (i, body') =