# HG changeset patch
# User blanchet
# Date 1409245630 -7200
# Node ID f9e4a9621c759d5d8ca14b2c5c3b9f7a73931b93
# Parent  32d3fa94ebb461a2087921bbd802dc81acf190b0
prefer '0.2 ms' to '249 \<mu>s'

diff -r 32d3fa94ebb4 -r f9e4a9621c75 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 28 19:02:37 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu Aug 28 19:07:10 2014 +0200
@@ -146,9 +146,9 @@
 fun string_of_ext_time (plus, time) =
   let val us = Time.toMicroseconds time in
     (if plus then "> " else "") ^
-    (if us < 1000 then signed_string_of_int us ^ " \<mu>s"
+    (if us < 1000 then string_of_real (Real.fromInt (us div 100) / 10.0) ^ " ms"
      else if us < 1000000 then signed_string_of_int (us div 1000) ^ " ms"
-     else string_of_real (0.1 * Real.fromInt (us div 100000)) ^ " s")
+     else string_of_real (Real.fromInt (us div 100000) / 10.0) ^ " s")
   end
 
 val string_of_time = string_of_ext_time o pair false