src/Pure/ML/ml_statistics_polyml-5.5.0.ML

--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Tue May 14 20:46:09 2013 +0200
@@ -51,8 +51,8 @@
      ("threads_wait_IO", Markup.print_int threadsWaitIO),
      ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
      ("threads_wait_signal", Markup.print_int threadsWaitSignal),
-     ("time_CPU", signed_string_of_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
-     ("time_GC", signed_string_of_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
+     ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+     ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
     user_counters
   end;