--- a/src/Pure/Concurrent/par_list.ML Fri Sep 19 21:00:50 2008 +0200
+++ b/src/Pure/Concurrent/par_list.ML Fri Sep 19 21:22:31 2008 +0200
@@ -32,8 +32,9 @@
| proper_exn (Exn.Exn exn) = SOME exn;
fun raw_map f xs =
- let val group = TaskQueue.new_group ()
- in Future.join_results (List.map (fn x => Future.future (SOME group) [] (fn () => f x)) xs) end;
+ let val group = TaskQueue.new_group () in
+ Future.join_results (List.map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs)
+ end;
fun map f xs =
let val results = raw_map f xs in