src/Pure/ML/ml_statistics.scala

     }
 
     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))
       }
     }
 
     private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized