diff -r d0331badb854 -r 0e40bd617b6c src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Sat Oct 18 17:29:39 2025 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Sat Oct 18 18:25:16 2025 +0200
@@ -78,7 +78,7 @@
       this.session = session
     }
 
-    override def exit(): Unit = synchronized {
+    override def exit(exit_state: Document.State): Unit = synchronized {
       session = null
       monitoring.cancel()
     }