changeset 55811 | aa1acc25126b |
parent 55803 | 74d3fe9031d8 |
child 55851 | 3d40cf74726c |
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Feb 28 22:00:13 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Feb 28 17:54:52 2014 +0100 @@ -232,7 +232,8 @@ fun co_rec_of [_, r] = r; fun time ctxt timer msg = (if Config.get ctxt bnf_timing - then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer)) + then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ + "ms") else (); Timer.startRealTimer ()); val preN = "pre_"