--- a/src/Pure/proofterm.ML Mon Jan 31 22:57:01 2011 +0100
+++ b/src/Pure/proofterm.ML Mon Jan 31 23:02:53 2011 +0100
@@ -1390,7 +1390,7 @@
else Future.map postproc body
| fulfill_proof_future thy promises postproc body =
singleton
- (Future.bulk {name = "Proofterm.fulfill_proof_future", group = NONE,
+ (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0})
(fn () =>
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1448,7 +1448,7 @@
else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
else
singleton
- (Future.bulk {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
+ (Future.forks {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1})
(make_body0 o full_proof0);
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);