--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Fri Mar 15 10:49:28 2013 +0100
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML Fri Mar 15 13:46:37 2013 +0100
@@ -51,10 +51,8 @@
("threads_wait_IO", Markup.print_int threadsWaitIO),
("threads_wait_mutex", Markup.print_int threadsWaitMutex),
("threads_wait_signal", Markup.print_int threadsWaitSignal),
- ("time_GC_system", signed_string_of_real (Time.toReal timeGCSystem)),
- ("time_GC_user", signed_string_of_real (Time.toReal timeGCUser)),
- ("time_non_GC_system", signed_string_of_real (Time.toReal timeNonGCSystem)),
- ("time_non_GC_user", signed_string_of_real (Time.toReal timeNonGCUser))] @
+ ("time_CPU", signed_string_of_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+ ("time_GC", signed_string_of_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
user_counters
end;