--- a/src/HOL/List.thy Tue Jun 17 14:11:40 2025 +0200
+++ b/src/HOL/List.thy Thu Jun 19 17:15:40 2025 +0200
@@ -8306,9 +8306,9 @@
intermediate lists on execution -- do not use for proving.
\<close>
-lemma map_filter_simps [code]:
+lemma map_filter_simps [simp, code, no_atp]:
+ \<open>map_filter f [] = []\<close>
\<open>map_filter f (x # xs) = (case f x of None \<Rightarrow> map_filter f xs | Some y \<Rightarrow> y # map_filter f xs)\<close>
- \<open>map_filter f [] = []\<close>
by (simp_all add: map_filter_def split: option.split)
lemma map_filter_map_filter [code_unfold]: