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') =