src/Pure/proofterm.ML

 
 fun fulfill_proof_future _ [] postproc body =
       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)));
 
 
 (***** abstraction over sort constraints *****)

     fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
     val body0 =
       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);
     val (i, body') =
       (*non-deterministic, depends on unknown promises*)