# HG changeset patch
# User wenzelm
# Date 1296511816 -3600
# Node ID 0f0f6212d6c6f2f9fc8917b527bbc058e4df71b9
# Parent  7da257539a8d4a3af787e0d2e3665c304d317d67
tuned trivial cases;

diff -r 7da257539a8d -r 0f0f6212d6c6 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Mon Jan 31 23:02:53 2011 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Mon Jan 31 23:10:16 2011 +0100
@@ -27,7 +27,10 @@
 struct
 
 fun managed_results name f xs =
-  if Multithreading.enabled () andalso not (Multithreading.self_critical ()) then
+  if null xs orelse null (tl xs) orelse
+      not (Multithreading.enabled ()) orelse Multithreading.self_critical ()
+  then map (Exn.capture f) xs
+  else
     let
       val group = Task_Queue.new_group (Future.worker_group ());
       val futures =
@@ -35,8 +38,7 @@
           (map (fn x => fn () => f x) xs);
       val results = Future.join_results futures
         handle exn => (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
-    in results end
-  else map (Exn.capture f) xs;
+    in results end;
 
 fun map f xs = Exn.release_first (managed_results "Par_List.map" f xs);