src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Sat Aug 20 09:42:34 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 20 15:52:29 2011 +0200
@@ -371,7 +371,7 @@
                         |> set_result result;
                     in ((assigns, execs, [(name, node')]), node') end)
               end))
-      |> Future.join_results |> Par_Exn.release_all |> map #1;
+      |> Future.joins |> map #1;
 
     val state' = state
       |> fold (fold define_exec o #2) updates