changeset 62685 | 1e5cf471e703 |
parent 62684 | cb20e8828196 |
child 62720 | 2ceae1e761bd |
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 22 07:18:36 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 22 07:57:01 2016 +0100 @@ -276,7 +276,7 @@ fun time ctxt timer msg = (if Config.get ctxt bnf_timing then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ - "ms") + " ms") else (); Timer.startRealTimer ()); val preN = "pre_"