--- a/src/Pure/PIDE/markup.ML Sat Sep 20 16:34:32 2025 +0200
+++ b/src/Pure/PIDE/markup.ML Sat Sep 20 16:39:35 2025 +0200
@@ -208,7 +208,6 @@
val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
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
val command_indentN: string val command_indent: int -> T
val goalN: string val goal: T
val subgoalN: string val subgoal: string -> T
@@ -714,9 +713,6 @@
(cpuN, Time.print cpu),
(gcN, Time.print gc)];
-val timingN = "timing";
-fun timing t = (timingN, timing_properties t);
-
(* command timing *)