src/Pure/ML-Systems/multithreading.ML

--- a/src/Pure/ML-Systems/multithreading.ML	Tue Nov 25 17:30:05 2014 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML	Wed Nov 26 11:43:51 2014 +0100
@@ -31,6 +31,7 @@
   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;
 
@@ -74,6 +75,8 @@
 fun NAMED_CRITICAL _ e = e ();
 fun CRITICAL e = e ();
 
+fun synchronized _ _ e = e ();
+
 
 (* serial numbers *)