1.1 --- a/src/Pure/ML-Systems/multithreading.ML	Sat Feb 16 16:43:59 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/multithreading.ML	Sat Feb 16 16:44:00 2008 +0100
     1.3 @@ -19,7 +19,6 @@
     1.4    val available: bool
     1.5    val max_threads: int ref
     1.6    val max_threads_value: unit -> int
     1.7 -  val managed_process: string -> string * bool
     1.8    val self_critical: unit -> bool
     1.9    datatype 'a task =
    1.10      Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
    1.11 @@ -42,12 +41,6 @@
    1.12  fun max_threads_value () = Int.max (! max_threads, 1);
    1.13  
    1.14  
    1.15 -(* managed external processes *)
    1.16 -
    1.17 -fun managed_process _ =
    1.18 -  raise Fail "No multithreading support -- cannot manage external processes";
    1.19 -
    1.20 -
    1.21  (* critical section *)
    1.22  
    1.23  fun self_critical () = false;