# HG changeset patch
# User wenzelm
# Date 1257376380 -3600
# Node ID 9348016909914941bc3412dd6bad7bacf5f98c9e
# Parent  cb409680dda887ba169f19a7d01acd65f60b65d8
revert fulfill_proof_future tuning (actually a bit slower due to granularity issues?);

diff -r cb409680dda8 -r 934801690991 src/Pure/proofterm.ML
--- 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);