src/Pure/ML-Systems/multithreading.ML

--- a/src/Pure/ML-Systems/multithreading.ML	Mon Dec 22 19:47:58 2014 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Mon Dec 22 20:40:37 2014 +0100
@@ -4,15 +4,8 @@
 Dummy implementation of multithreading setup.
 *)
 
-signature BASIC_MULTITHREADING =
-sig
-  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
-  val CRITICAL: (unit -> 'a) -> 'a
-end;
-
 signature MULTITHREADING =
 sig
-  include BASIC_MULTITHREADING
   val available: bool
   val max_threads_value: unit -> int
   val max_threads_update: int -> unit
@@ -30,7 +23,6 @@
   val tracing: int -> (unit -> string) -> unit
   val tracing_time: bool -> Time.time -> (unit -> string) -> unit
   val real_time: ('a -> unit) -> 'a -> Time.time
-  val self_critical: unit -> bool
   val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
   val serial: unit -> int
 end;
@@ -69,11 +61,7 @@
 fun real_time f x = (f x; Time.zeroTime);
 
 
-(* critical section *)
-
-fun self_critical () = false;
-fun NAMED_CRITICAL _ e = e ();
-fun CRITICAL e = e ();
+(* synchronized evaluation *)
 
 fun synchronized _ _ e = e ();
 
@@ -85,5 +73,3 @@
 
 end;
 
-structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
-open Basic_Multithreading;