--- a/src/Pure/proofterm.ML Wed Nov 04 21:22:35 2009 +0100
+++ b/src/Pure/proofterm.ML Thu Nov 05 00:13:00 2009 +0100
@@ -1296,8 +1296,6 @@
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);