src/Pure/ML/ml_statistics.scala

--- a/src/Pure/ML/ml_statistics.scala	Sat Aug 15 13:37:34 2020 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Sat Aug 15 13:45:25 2020 +0200
@@ -80,7 +80,7 @@
 
   /* protocol handler */
 
-  class Protocol_Handler extends Session.Protocol_Handler
+  class Handler extends Session.Protocol_Handler
   {
     private var session: Session = null
     private var monitoring: Future[Unit] = Future.value(())