src/Pure/proofterm.ML
changeset 41673 1c191a39549f
parent 41672 2f70b1ddd09f
child 41674 7da257539a8d
     1.1 --- a/src/Pure/proofterm.ML	Mon Jan 31 21:54:49 2011 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Mon Jan 31 22:57:01 2011 +0100
     1.3 @@ -1390,7 +1390,7 @@
     1.4        else Future.map postproc body
     1.5    | fulfill_proof_future thy promises postproc body =
     1.6        singleton
     1.7 -        (Future.bulk {group = NONE,
     1.8 +        (Future.bulk {name = "Proofterm.fulfill_proof_future", group = NONE,
     1.9              deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
    1.10          (fn () =>
    1.11            postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
    1.12 @@ -1446,7 +1446,10 @@
    1.13      val body0 =
    1.14        if ! proofs <> 2 then Future.value (make_body0 MinProof)
    1.15        else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
    1.16 -      else Future.fork_pri ~1 (make_body0 o full_proof0);
    1.17 +      else
    1.18 +        singleton
    1.19 +          (Future.bulk {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
    1.20 +          (make_body0 o full_proof0);
    1.21  
    1.22      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    1.23      val (i, body') =