# HG changeset patch
# User wenzelm
# Date 1524560838 -7200
# Node ID a8ee8e4884ecbf697f1b36c6b3a80207dee956bf
# Parent  7fb7a6366a40eddaa3113fc973e789228f6d365e
less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);

diff -r 7fb7a6366a40 -r a8ee8e4884ec src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Apr 24 11:03:51 2018 +0200
+++ b/src/Pure/proofterm.ML	Tue Apr 24 11:07:18 2018 +0200
@@ -1610,14 +1610,16 @@
     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}
-          (fn () =>
-            make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf))));
+          make_body;
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
     val (i, body') =