diff -r f4441890dee0 -r 0a3d61228714 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat May 31 21:51:08 2025 +0200
+++ b/src/HOL/Set.thy	Sun Jun 01 10:29:45 2025 +0200
@@ -17,7 +17,7 @@
 axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" \<comment> \<open>comprehension\<close>
   and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> \<open>membership\<close>
   where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
-    and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
+    and Collect_mem_eq [simp, code_unfold]: "Collect (\<lambda>x. member x A) = A"
 
 notation
   member  (\<open>'(\<in>')\<close>) and