diff -r 6adf6cc82013 -r a2486a4b42da src/HOL/Data_Structures/Selection.thy
--- a/src/HOL/Data_Structures/Selection.thy	Fri Aug 23 18:40:12 2024 +0200
+++ b/src/HOL/Data_Structures/Selection.thy	Mon Aug 26 18:26:00 2024 +0200
@@ -633,9 +633,7 @@
 
 subsection \<open>Running time analysis\<close>
 
-fun T_partition3 :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
-  "T_partition3 x [] = 1"
-| "T_partition3 x (y # ys) = T_partition3 x ys + 1"
+time_fun partition3 equations partition3_code
 
 lemma T_partition3_eq: "T_partition3 x xs = length xs + 1"
   by (induction x xs rule: T_partition3.induct) auto