changeset 52031 | 9a9238342963 |
parent 51918 | 3c152334f794 |
child 52207 | 21026c312cc3 |
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 16 13:19:27 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 16 13:34:13 2013 +0200 @@ -219,7 +219,7 @@ val timing = true; fun time timer msg = (if timing - then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer)) + then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer)) else (); Timer.startRealTimer ()); val preN = "pre_"