unused;

--- a/src/Pure/PIDE/markup.ML	Thu Aug 06 22:58:18 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Aug 06 23:13:24 2020 +0200
@@ -165,7 +165,6 @@
   val cpuN: string
   val gcN: string
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
-  val command_timingN: string
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
   val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
@@ -591,8 +590,6 @@
 
 (* command timing *)
 
-val command_timingN = "command_timing";
-
 fun parse_command_timing_properties props =
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>