# HG changeset patch
# User wenzelm
# Date 1253460203 -7200
# Node ID fef7022dc5ab3a08be437715a227b0fba426a6a6
# Parent  0bc4f7e3e2d3e32f165058084569666e034b9559
actually observe Multithreading.enabled (cf. d302f1c9e356);

diff -r 0bc4f7e3e2d3 -r fef7022dc5ab src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Sat Sep 19 10:19:34 2009 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Sun Sep 20 17:23:23 2009 +0200
@@ -27,8 +27,10 @@
 struct
 
 fun raw_map f xs =
-  let val group = Task_Queue.new_group (Future.worker_group ())
-  in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end;
+  if Multithreading.enabled () then
+    let val group = Task_Queue.new_group (Future.worker_group ())
+    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
+  else map (Exn.capture f) xs;
 
 fun map f xs = Exn.release_first (raw_map f xs);