# HG changeset patch
# User wenzelm
# Date 1267273915 -3600
# Node ID 2f83aa48d6967b7ab3af715ae9b1dfcac5da9047
# Parent  5da5ac6c6b771b76b14ea183058cad33845c8db7
degrade gracefully in CRITICAL section;

diff -r 5da5ac6c6b77 -r 2f83aa48d696 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Fri Feb 26 23:08:45 2010 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Sat Feb 27 13:31:55 2010 +0100
@@ -27,7 +27,7 @@
 struct
 
 fun raw_map f xs =
-  if Multithreading.enabled () then
+  if Multithreading.enabled () andalso not (Multithreading.self_critical ()) 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;