src/Pure/ML-Systems/multithreading.ML

   val trace: int ref
   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;
 
 structure Multithreading: MULTITHREADING =
 struct

 
 fun self_critical () = false;
 fun NAMED_CRITICAL _ e = e ();
 fun CRITICAL e = e ();
 
+fun synchronized _ _ e = e ();
+
 
 (* serial numbers *)
 
 local val count = ref (0: int)
 in fun serial () = (count := ! count + 1; ! count) end;