src/Pure/PIDE/markup.scala

 
   object ML_Statistics
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
-        case (FUNCTION, "ML_statistics") :: stats => Some(stats)
+        case (FUNCTION, "ML_statistics") :: props => Some(props)
         case _ => None
       }
   }
 
   object Task_Statistics
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
-        case (FUNCTION, "task_statistics") :: stats => Some(stats)
+        case (FUNCTION, "task_statistics") :: props => Some(props)
         case _ => None
       }
   }
 
   val LOADING_THEORY = "loading_theory"