diff -r e2ae4a6cf166 -r 605a3b1ef6ba src/Pure/Concurrent/par_list.ML --- a/src/Pure/Concurrent/par_list.ML Tue Oct 21 15:01:16 2008 +0200 +++ b/src/Pure/Concurrent/par_list.ML Tue Oct 21 15:01:18 2008 +0200 @@ -28,7 +28,7 @@ struct fun raw_map f xs = - if ! future_scheduler andalso Multithreading.enabled () then + if Future.enabled () then let val group = TaskQueue.new_group (); val futures = map (fn x => Future.future (SOME group) [] true (fn () => f x)) xs;