--- 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