diff -r 9c47740e974a -r 21a493abde0f src/HOL/Data_Structures/Array_Braun.thy
--- a/src/HOL/Data_Structures/Array_Braun.thy	Wed Nov 06 16:27:06 2024 +0100
+++ b/src/HOL/Data_Structures/Array_Braun.thy	Wed Nov 06 18:10:39 2024 +0100
@@ -509,7 +509,7 @@
 
 lemma T_brauns_simple: "T_brauns k xs = (if xs = [] then 0 else
    3 * (min (2^k) (length xs) + 1) + (min (2^k) (length xs - 2^k) + 1) + T_brauns (k+1) (drop (2^k) xs)) + 1"
-by(simp add: T_nodes T_take_eq T_drop_eq length_brauns min_def)
+by(simp add: T_nodes T_take T_drop length_brauns min_def)
 
 theorem T_brauns_ub:
   "T_brauns k xs \<le> 9 * (length xs + 1)"