# HG changeset patch
# User wenzelm
# Date 1602765725 -7200
# Node ID 5bf00b1dd7d89b4710a7ffffe2caf150258d6ed0
# Parent  b772a93d44aa808aa39cb6a5c4fdd1bc31021779
more standard Value.print_time;

diff -r b772a93d44aa -r 5bf00b1dd7d8 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Thu Oct 15 14:31:55 2020 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Oct 15 14:42:05 2020 +0200
@@ -96,8 +96,8 @@
 
     val output = drop_suffix (equal "") res
     val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output
-    val _ = SMT_Config.trace_msg ctxt (pretty "Time (ms):") [\<^make_string> (Time.toMilliseconds elapsed)]
-    val _ = SMT_Config.statistics_msg ctxt (pretty "Time (ms):") [\<^make_string> (Time.toMilliseconds elapsed)]
+    val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
+    val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"]
 
     val _ = member (op =) normal_return_codes return_code orelse
       raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)