# HG changeset patch
# User wenzelm
# Date 1460204912 -7200
# Node ID bb2b8e915243dccb59526ea138751d7c6821c406
# Parent  9ff9bcbc23410bb9eba3427f466d02e77c582029
tuned signature;

diff -r 9ff9bcbc2341 -r bb2b8e915243 src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:21:29 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:28:32 2016 +0200
@@ -14,7 +14,6 @@
   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;
 
@@ -77,13 +76,6 @@
     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 *)
 
@@ -95,7 +87,9 @@
         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) ();