1.1 --- a/src/HOL/ex/ROOT.ML	Wed Jun 02 12:40:25 2010 +0200
     1.2 +++ b/src/HOL/ex/ROOT.ML	Wed Jun 02 13:18:48 2010 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  HTML.with_charset "utf-8" (no_document use_thys)
     1.5    ["Hebrew", "Chinese", "Serbian"];
     1.6  
     1.7 -(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
     1.8 +(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
     1.9    "Hilbert_Classical";
    1.10  
    1.11  use_thy "SVC_Oracle";

     2.1 --- a/src/Pure/proofterm.ML	Wed Jun 02 12:40:25 2010 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Wed Jun 02 13:18:48 2010 +0200
     2.3 @@ -1387,10 +1387,12 @@
     2.4      val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
     2.5    in PBody {oracles = oracles, thms = thms, proof = proof} end;
     2.6  
     2.7 -fun fulfill_proof_future _ [] postproc body = Future.value (postproc body)
     2.8 +fun fulfill_proof_future _ [] postproc body =
     2.9 +      if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
    2.10 +      else Future.map postproc body
    2.11    | fulfill_proof_future thy promises postproc body =
    2.12 -      Future.fork_deps (map snd promises) (fn () =>
    2.13 -        postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) body));
    2.14 +      Future.fork_deps (body :: map snd promises) (fn () =>
    2.15 +        postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
    2.16  
    2.17  
    2.18  (***** abstraction over sort constraints *****)
    2.19 @@ -1442,11 +1444,14 @@
    2.20        else (I, [], prop, args);
    2.21      val argsP = ofclasses @ map Hyp hyps;
    2.22  
    2.23 -    val proof0 =
    2.24 -      if ! proofs = 2 then
    2.25 -        #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
    2.26 -      else MinProof;
    2.27 -    val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    2.28 +    fun full_proof0 () =
    2.29 +      #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
    2.30 +
    2.31 +    fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    2.32 +    val body0 =
    2.33 +      if ! proofs <> 2 then Future.value (make_body0 MinProof)
    2.34 +      else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
    2.35 +      else Future.fork_pri ~1 (make_body0 o full_proof0);
    2.36  
    2.37      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    2.38      val (i, body') =