diff -r c998827f1df9 -r 7773ec172572 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Aug 07 21:21:44 2020 +0200
+++ b/src/Pure/Tools/build.scala	Fri Aug 07 22:19:32 2020 +0200
@@ -316,10 +316,14 @@
                 fun(Markup.Command_Timing.name, command_timings, command_timing),
                 fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
                 fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
-                fun(Markup.ML_Statistics.name, runtime_statistics, Markup.ML_Statistics.unapply),
                 fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
           })
 
+        session.runtime_statistics += Session.Consumer("ML_statistics")
+          {
+            case Session.Runtime_Statistics(props) => runtime_statistics += props
+          }
+
         session.all_messages += Session.Consumer[Any]("build_session_output")
           {
             case msg: Prover.Output =>