src/Pure/Concurrent/future.ML
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;