# HG changeset patch
# User blanchet
# Date 1409237907 -7200
# Node ID aa239fee063a9f6c4b3e12b8d8afa0b695923bb8
# Parent  42e998248ddc53da35192188e01a75b117d0b0bf
show microseconds as well (useful when playing with Isar proofs)

diff -r 42e998248ddc -r aa239fee063a src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -144,14 +144,11 @@
   end
 
 fun string_of_ext_time (plus, time) =
-  let val ms = Time.toMilliseconds time in
+  let val us = Time.toMicroseconds time in
     (if plus then "> " else "") ^
-    (if plus andalso ms mod 1000 = 0 then
-       signed_string_of_int (ms div 1000) ^ " s"
-     else if ms < 1000 then
-       signed_string_of_int ms ^ " ms"
-     else
-       string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
+    (if us < 1000 then signed_string_of_int us ^ " \<mu>s"
+     else if us < 1000000 then signed_string_of_int (us div 1000) ^ " ms"
+     else string_of_real (0.1 * Real.fromInt (us div 10000)) ^ " s")
   end
 
 val string_of_time = string_of_ext_time o pair false