src/HOL/Data_Structures/Time_Funs.thy

--- a/src/HOL/Data_Structures/Time_Funs.thy	Thu Jul 18 16:00:40 2024 +0200
+++ b/src/HOL/Data_Structures/Time_Funs.thy	Mon Jul 29 15:26:03 2024 +0200
@@ -23,10 +23,7 @@
 
 lemmas [simp del] = T_length.simps
 
-
-fun T_map  :: "('a \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> nat" where
-  "T_map T_f [] = 1"
-| "T_map T_f (x # xs) = T_f x + T_map T_f xs + 1"
+time_fun map
 
 lemma T_map_eq: "T_map T_f xs = (\<Sum>x\<leftarrow>xs. T_f x) + length xs + 1"
   by (induction xs) auto