diff -r 2f70c60cdbb2 -r 8b4340d82248 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/List.thy	Mon Dec 23 19:38:16 2024 +0100
@@ -4429,7 +4429,7 @@
   have 1: "x \<notin> set ?pref" by (metis (full_types) set_takeWhileD)
   have 2: "xs = ?pref @ x # tl ?rest"
     by (metis rest append_eq_conv_conj hd_Cons_tl takeWhile_eq_take)
-  have "count_list (tl ?rest) x = n"using [[metis_suggest_of]]
+  have "count_list (tl ?rest) x = n"
     using assms rest 1 2 count_notin count_list_append[of ?pref "x # tl ?rest" x] by simp
   with 1 2 show ?thesis by blast
 qed