# HG changeset patch
# User wenzelm
# Date 1224600779 -7200
# Node ID 3a8d75c935ce150db2f9f88cf350ae4a27de65b2
# Parent  605a3b1ef6ba0875dc52f294f9d2ddb41ba73c20
Future.join_result;

diff -r 605a3b1ef6ba -r 3a8d75c935ce src/Pure/Concurrent/par_list.ML
--- 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;