diff -r 5f388e514ab8 -r 77ef8bef0593 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Thu Mar 04 19:55:52 2021 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Thu Mar 04 21:04:27 2021 +0100
@@ -93,7 +93,7 @@
     override def exit(): Unit = synchronized
     {
       session = null
-      monitoring.cancel
+      monitoring.cancel()
     }
 
     private def consume(props: Properties.T): Unit = synchronized