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