subject to Multithreading.enabled;
raw_map: join sequentially, less overhead;

--- a/src/Pure/Concurrent/par_list.ML	Thu Oct 09 20:53:15 2008 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Thu Oct 09 20:53:16 2008 +0200
@@ -28,9 +28,13 @@
 struct
 
 fun raw_map f xs =
-  let val group = TaskQueue.new_group () in
-    Future.join_results (List.map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs)
-  end;
+  if ! future_scheduler andalso Multithreading.enabled () then
+    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;
+    in Future.join_results futures end
+  else map (Exn.capture f) xs;
 
 fun map f xs = Exn.release_first (raw_map f xs);