src/Pure/Concurrent/multithreading.ML

   val sync_wait: Thread.threadAttribute list option -> Time.time option ->
     ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result
   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 synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
 end;
 
 structure Multithreading: MULTITHREADING =
 struct

     else if time >= seconds 1.0 then 1
     else if time >= seconds 0.1 then 2
     else if time >= seconds 0.01 then 3
     else if time >= seconds 0.001 then 4 else 5);
 
-fun real_time f x =
-  let
-    val timer = Timer.startRealTimer ();
-    val () = f x;
-    val time = Timer.checkRealTimer timer;
-  in time end;
-
 
 (* synchronized evaluation *)
 
 fun synchronized name lock e =
   Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>

       val immediate =
         if Mutex.trylock lock then true
         else
           let
             val _ = tracing 5 (fn () => name ^ ": locking ...");
-            val time = real_time Mutex.lock lock;
+            val timer = Timer.startRealTimer ();
+            val _ = Mutex.lock lock;
+            val time = Timer.checkRealTimer timer;
             val _ = tracing_time true time (fn () => name ^ ": locked after " ^ Time.toString time);
           in false end;
       val result = Exn.capture (restore_attributes e) ();
       val _ = if immediate then () else tracing 5 (fn () => name ^ ": unlocking ...");
       val _ = Mutex.unlock lock;