diff -r 26a0984191b3 -r 2ad5c46bcd04 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jan 24 17:31:12 2013 +0100
+++ b/src/Pure/proofterm.ML	Thu Jan 24 21:18:30 2013 +0100
@@ -1399,18 +1399,22 @@
     val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
   in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
-fun fulfill_proof_future _ [] postproc body = Future.map postproc body
-  | fulfill_proof_future thy promises postproc body =
-      if Context.is_draft thy then
-        Future.value
-          (postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body)))
-      else
-        (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)));
+fun fulfill_proof_future thy promises postproc body =
+  let
+    fun fulfill () =
+      postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body));
+  in
+    if null promises then Future.map postproc body
+    else if Context.is_draft thy then Future.value (fulfill ())
+    else if Future.is_finished body andalso length promises = 1 then
+      Future.map (fn _ => fulfill ()) (snd (hd promises))
+    else
+      (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}
+        fulfill
+  end;
 
 
 (***** abstraction over sort constraints *****)