1.1 --- a/src/Pure/proofterm.ML	Wed Jun 02 08:01:45 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed Jun 02 11:09:26 2010 +0200
     1.3 @@ -1387,10 +1387,12 @@
     1.4      val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
     1.5    in PBody {oracles = oracles, thms = thms, proof = proof} end;
     1.6  
     1.7 -fun fulfill_proof_future _ [] postproc body = Future.value (postproc body)
     1.8 +fun fulfill_proof_future _ [] postproc body =
     1.9 +      if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
    1.10 +      else Future.map postproc body
    1.11    | fulfill_proof_future thy promises postproc body =
    1.12 -      Future.fork_deps (map snd promises) (fn () =>
    1.13 -        postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) body));
    1.14 +      Future.fork_deps (body :: map snd promises) (fn () =>
    1.15 +        postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
    1.16  
    1.17  
    1.18  (***** abstraction over sort constraints *****)
    1.19 @@ -1442,11 +1444,14 @@
    1.20        else (I, [], prop, args);
    1.21      val argsP = ofclasses @ map Hyp hyps;
    1.22  
    1.23 -    val proof0 =
    1.24 -      if ! proofs = 2 then
    1.25 -        #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
    1.26 -      else MinProof;
    1.27 -    val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    1.28 +    fun full_proof0 () =
    1.29 +      #4 (shrink_proof [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)));
    1.30 +
    1.31 +    fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    1.32 +    val body0 =
    1.33 +      if ! proofs <> 2 then Future.value (make_body0 MinProof)
    1.34 +      else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
    1.35 +      else Future.fork_pri ~1 (make_body0 o full_proof0);
    1.36  
    1.37      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    1.38      val (i, body') =