--- a/src/Pure/Concurrent/par_list.ML Tue Jul 28 16:28:49 2009 +0200
+++ b/src/Pure/Concurrent/par_list.ML Tue Jul 28 16:30:23 2009 +0200
@@ -27,10 +27,8 @@
struct
fun raw_map f xs =
- if Future.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;
+ 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;
fun map f xs = Exn.release_first (raw_map f xs);