src/HOL/TPTP/TPTP_Interpret_Test.thy
changeset 82086 e0edf30885ef
parent 72511 460d743010bc
--- 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