src/Pure/ML-Systems/multithreading.ML

--- a/src/Pure/ML-Systems/multithreading.ML	Sat Feb 16 16:43:59 2008 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Sat Feb 16 16:44:00 2008 +0100
@@ -19,7 +19,6 @@
   val available: bool
   val max_threads: int ref
   val max_threads_value: unit -> int
-  val managed_process: string -> string * bool
   val self_critical: unit -> bool
   datatype 'a task =
     Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
@@ -42,12 +41,6 @@
 fun max_threads_value () = Int.max (! max_threads, 1);
 
 
-(* managed external processes *)
-
-fun managed_process _ =
-  raise Fail "No multithreading support -- cannot manage external processes";
-
-
 (* critical section *)
 
 fun self_critical () = false;