# HG changeset patch # User wenzelm # Date 1257366065 -3600 # Node ID 4b403f72a511cdba3c93ad3a998e37fc16f2eea7 # Parent a07558eb50298fc0bf521553f2d9e99ac377b89b fulfill_proof_future: tuned important special case of singleton promise; diff -r a07558eb5029 -r 4b403f72a511 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Wed Nov 04 20:31:36 2009 +0100 +++ b/src/Pure/proofterm.ML Wed Nov 04 21:21:05 2009 +0100 @@ -1296,6 +1296,8 @@ in PBody {oracles = oracles, thms = thms, proof = proof} end; fun fulfill_proof_future _ [] body = Future.value body + | fulfill_proof_future thy [(i, promise)] body = + Future.map (fn p => fulfill_proof thy [(i, p)] body) promise | fulfill_proof_future thy promises body = Future.fork_deps (map snd promises) (fn () => fulfill_proof thy (map (apsnd Future.join) promises) body);