cache props;

--- a/src/Pure/ML/ml_statistics.scala	Fri Aug 07 22:19:32 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Fri Aug 07 22:23:40 2020 +0200
@@ -71,7 +71,8 @@
     private def consume(props: Properties.T): Unit = synchronized
     {
       if (session != null && session.session_options.bool("ML_statistics")) {
-        session.runtime_statistics.post(Session.Runtime_Statistics(props))
+        val stats = Session.Runtime_Statistics(session.xml_cache.props(props))
+        session.runtime_statistics.post(stats)
       }
     }