1.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 28 16:28:49 2009 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jul 28 16:30:23 2009 +0200
     1.3 @@ -27,7 +27,6 @@
     1.4  
     1.5  signature FUTURE =
     1.6  sig
     1.7 -  val enabled: unit -> bool
     1.8    type task = Task_Queue.task
     1.9    type group = Task_Queue.group
    1.10    val is_worker: unit -> bool
    1.11 @@ -57,11 +56,6 @@
    1.12  
    1.13  (** future values **)
    1.14  
    1.15 -fun enabled () =
    1.16 -  Multithreading.enabled () andalso
    1.17 -    not (Multithreading.self_critical ());
    1.18 -
    1.19 -
    1.20  (* identifiers *)
    1.21  
    1.22  type task = Task_Queue.task;

     2.1 --- a/src/Pure/Concurrent/par_list.ML	Tue Jul 28 16:28:49 2009 +0200
     2.2 +++ b/src/Pure/Concurrent/par_list.ML	Tue Jul 28 16:30:23 2009 +0200
     2.3 @@ -27,10 +27,8 @@
     2.4  struct
     2.5  
     2.6  fun raw_map f xs =
     2.7 -  if Future.enabled () then
     2.8 -    let val group = Task_Queue.new_group (Future.worker_group ())
     2.9 -    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
    2.10 -  else map (Exn.capture f) xs;
    2.11 +  let val group = Task_Queue.new_group (Future.worker_group ())
    2.12 +  in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end;
    2.13  
    2.14  fun map f xs = Exn.release_first (raw_map f xs);
    2.15  

     3.1 --- a/src/Pure/goal.ML	Tue Jul 28 16:28:49 2009 +0200
     3.2 +++ b/src/Pure/goal.ML	Tue Jul 28 16:30:23 2009 +0200
     3.3 @@ -103,7 +103,7 @@
     3.4  val parallel_proofs = ref 1;
     3.5  
     3.6  fun future_enabled () =
     3.7 -  Future.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
     3.8 +  Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
     3.9  
    3.10  fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
    3.11