diff -r a6cbf8ce979e -r 53e8858b839f src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Aug 26 15:59:21 2020 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Thu Aug 27 12:34:10 2020 +0200
@@ -117,7 +117,7 @@
       }
     }
 
-    val functions = List(Markup.ML_Statistics.name -> ml_statistics)
+    override val functions = List(Markup.ML_Statistics.name -> ml_statistics)
   }