Future.join_result;

--- a/src/Pure/Concurrent/par_list.ML	Tue Oct 21 15:01:18 2008 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Tue Oct 21 16:52:59 2008 +0200
@@ -32,7 +32,7 @@
     let
       val group = TaskQueue.new_group ();
       val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;
-      val _ = List.app (ignore o Future.join_results o single) futures;
+      val _ = List.app (ignore o Future.join_result) futures;
     in Future.join_results futures end
   else map (Exn.capture f) xs;