# HG changeset patch
# User blanchet
# Date 1409239556 -7200
# Node ID f9ff405162a13106fd979f4b2576b23947ad7e1e
# Parent  ee65e9cfe284234cded61a5bb99964cf19b10723
fixed second computations

diff -r ee65e9cfe284 -r f9ff405162a1 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 17:25:56 2014 +0200
@@ -148,7 +148,7 @@
     (if plus then "> " else "") ^
     (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")
+     else string_of_real (0.1 * Real.fromInt (us div 100000)) ^ " s")
   end
 
 val string_of_time = string_of_ext_time o pair false