src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Thu Sep 10 21:07:58 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Thu Sep 10 21:14:50 2020 +0200
@@ -99,7 +99,7 @@
     private def consume(props: Properties.T): Unit = synchronized
     {
       if (session != null) {
-        val props1 = (session.xml_cache.props(props ::: Platform.jvm_statistics()))
+        val props1 = (session.xml_cache.props(props ::: Java_Statistics.jvm_statistics()))
         session.runtime_statistics.post(Session.Runtime_Statistics(props1))
       }
     }