changeset 32255 | d302f1c9e356 |
parent 32253 | d9def420c84e |
child 32286 | 1fb5db48002d |
--- a/src/Pure/Concurrent/future.ML Tue Jul 28 16:28:49 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Tue Jul 28 16:30:23 2009 +0200 @@ -27,7 +27,6 @@ signature FUTURE = sig - val enabled: unit -> bool type task = Task_Queue.task type group = Task_Queue.group val is_worker: unit -> bool @@ -57,11 +56,6 @@ (** future values **) -fun enabled () = - Multithreading.enabled () andalso - not (Multithreading.self_critical ()); - - (* identifiers *) type task = Task_Queue.task;