src/HOL/Tools/Nitpick/nitpick.ML
changeset 52031 9a9238342963
parent 50830 fc4025435b51
child 52202 d5c80b12a1f2
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 16 13:19:27 2013 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 16 13:34:13 2013 +0200
     1.3 @@ -1051,7 +1051,7 @@
     1.4               (print_nt (fn () => excipit "ran out of time after checking");
     1.5                if !met_potential > 0 then potentialN else unknownN)
     1.6      val _ = print_v (fn () =>
     1.7 -                "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
     1.8 +                "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
     1.9                  ".")
    1.10    in (outcome_code, !state_ref) end
    1.11