# HG changeset patch
# User wenzelm
# Date 1738784782 -3600
# Node ID e0edf30885ef8ed5a4d75a52edb480741e4242b0
# Parent  c0f4968fa96ef5dfd63c28db88a462bdad1b3f32
tuned signature: more explicit operations;

diff -r c0f4968fa96e -r e0edf30885ef src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Feb 05 13:00:04 2025 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Wed Feb 05 20:46:22 2025 +0100
@@ -133,7 +133,7 @@
           else
             (warning (" test: file " ^ Path.print file ^
              " raised exception: " ^ Runtime.exn_message exn);
-             {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
+             Timing.zero)
       val to_real = Time.toReal
       val diff_elapsed =
         #elapsed t2 - #elapsed t1
diff -r c0f4968fa96e -r e0edf30885ef src/Pure/General/timing.ML
--- a/src/Pure/General/timing.ML	Wed Feb 05 13:00:04 2025 +0100
+++ b/src/Pure/General/timing.ML	Wed Feb 05 20:46:22 2025 +0100
@@ -16,6 +16,7 @@
 sig
   include BASIC_TIMING
   type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
+  val zero: timing
   type start
   val start: unit -> start
   val result: start -> timing
@@ -34,6 +35,8 @@
 
 type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};
 
+val zero: timing = {elapsed = Time.zeroTime, cpu = Time.zeroTime, gc = Time.zeroTime};
+
 
 (* timer control *)