src/Pure/proofterm.ML
changeset 41672 2f70b1ddd09f
parent 39687 4e9b6ada3a21
child 41673 1c191a39549f
     1.1 --- a/src/Pure/proofterm.ML	Mon Jan 31 17:19:23 2011 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Mon Jan 31 21:54:49 2011 +0100
     1.3 @@ -1389,8 +1389,11 @@
     1.4        if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
     1.5        else Future.map postproc body
     1.6    | fulfill_proof_future thy promises postproc body =
     1.7 -      Future.fork_deps (body :: map snd promises) (fn () =>
     1.8 -        postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
     1.9 +      singleton
    1.10 +        (Future.bulk {group = NONE,
    1.11 +            deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
    1.12 +        (fn () =>
    1.13 +          postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
    1.14  
    1.15  
    1.16  (***** abstraction over sort constraints *****)