--- a/src/Pure/proofterm.ML Fri Aug 19 17:39:37 2011 +0200
+++ b/src/Pure/proofterm.ML Fri Aug 19 18:01:23 2011 +0200
@@ -1402,10 +1402,10 @@
if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
else Future.map postproc body
| fulfill_proof_future thy promises postproc body =
- singleton
- (Future.forks {name = "Proofterm.fulfill_proof_future", group = NONE,
- deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
- interrupts = true})
+ (singleton o Future.forks)
+ {name = "Proofterm.fulfill_proof_future", group = NONE,
+ deps = Future.task_of body :: map (Future.task_of o snd) promises, pri = 0,
+ interrupts = true}
(fn () =>
postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)));
@@ -1461,10 +1461,9 @@
if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
else
- singleton
- (Future.forks
- {name = "Proofterm.prepare_thm_proof", group = NONE, deps = [], pri = ~1,
- interrupts = true})
+ (singleton o Future.forks)
+ {name = "Proofterm.prepare_thm_proof", group = NONE,
+ deps = [], pri = ~1, interrupts = true}
(make_body0 o full_proof0);
fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);