src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Sat Jan 02 20:56:08 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sat Jan 02 22:22:34 2021 +0100
@@ -99,7 +99,7 @@
     private def consume(props: Properties.T): Unit = synchronized
     {
       if (session != null) {
-        val props1 = (session.xml_cache.props(props ::: Java_Statistics.jvm_statistics()))
+        val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics()))
         session.runtime_statistics.post(Session.Runtime_Statistics(props1))
       }
     }