thm_proof: recovered single-threaded version;
authorwenzelm
Tue Jan 27 14:28:51 2009 +0100 (2009-01-27)
changeset 29642be22ba214475
parent 29641 08d462dbb1a9
child 29643 5e0df4b6849e
thm_proof: recovered single-threaded version;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Tue Jan 27 13:52:32 2009 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Tue Jan 27 14:28:51 2009 +0100
     1.3 @@ -1227,6 +1227,11 @@
     1.4          val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
     1.5        in PBody {oracles = oracles, thms = thms, proof = proof} end;
     1.6  
     1.7 +fun fulfill_proof_future _ [] body = Future.value body
     1.8 +  | fulfill_proof_future thy promises body =
     1.9 +      Future.fork_deps (map snd promises) (fn () =>
    1.10 +        fulfill_proof thy (map (apsnd Future.join) promises) body);
    1.11 +
    1.12  
    1.13  (***** theorems *****)
    1.14  
    1.15 @@ -1243,12 +1248,9 @@
    1.16        if ! proofs = 2 then
    1.17          #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
    1.18        else MinProof;
    1.19 +    val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    1.20  
    1.21 -    fun new_prf () = (serial (), name, prop,
    1.22 -      Future.fork_deps (map snd promises) (fn () =>
    1.23 -        fulfill_proof thy (map (apsnd Future.join) promises)
    1.24 -          (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
    1.25 -
    1.26 +    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
    1.27      val (i, name, prop, body') =
    1.28        (case strip_combt (fst (strip_combP prf)) of
    1.29          (PThm (i, ((old_name, prop', NONE), body')), args') =>