diff -r 3ce619d8d432 -r 9d7ea903e877 src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Thu Dec 04 23:46:20 2008 +0100 +++ b/src/Pure/Concurrent/par_list.ML Thu Dec 04 23:46:20 2008 +0100 @@ -31,7 +31,7 @@ if Future.enabled () then let val group = TaskQueue.new_group (); - val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs; + val futures = map (fn x => Future.fork_group group (fn () => f x)) xs; val _ = List.app (ignore o Future.join_result) futures; in Future.join_results futures end else map (Exn.capture f) xs;