src/Pure/PIDE/markup.scala

         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
-  object ML_Pid extends Function("ML_pid")
+  object ML_Statistics extends Function("ML_statistics")
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
-        case List(PROPERTY, (ID, Value.Long(pid))) => Some(pid)
+        case List(PROPERTY, ("pid", Value.Long(pid))) => Some(pid)
         case _ => None
       }
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)

   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
   {
     val Threads = new Properties.Int("threads")
   }
-  object ML_Statistics extends Properties_Function("ML_statistics")
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Name_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")