diff -r f1c29e366c09 -r 4aeb25ba90f3 src/HOL/Data_Structures/Queue_2Lists.thy
--- a/src/HOL/Data_Structures/Queue_2Lists.thy	Sun Mar 24 14:15:10 2024 +0100
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy	Sun Mar 24 14:50:47 2024 +0100
@@ -59,10 +59,10 @@
 
 text \<open>Running times:\<close>
 
-define_time_fun norm
-define_time_fun enq
-define_time_fun tl
-define_time_fun deq
+time_fun norm
+time_fun enq
+time_fun tl
+time_fun deq
 
 lemma T_tl_0: "T_tl xs = 0"
 by(cases xs)auto