diff -r bd951e02d6b9 -r e9f3b94eb6a0 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat May 24 09:06:26 2025 +0200
+++ b/src/HOL/List.thy	Wed May 28 17:49:22 2025 +0200
@@ -8257,7 +8257,7 @@
 
 lemma is_empty_set [code]:
   "Set.is_empty (set xs) \<longleftrightarrow> List.null xs"
-  by (simp add: Set.is_empty_def null_def)
+  by (simp add: null_def)
 
 lemma empty_set [code]:
   "{} = set []"
@@ -8288,7 +8288,7 @@
 lemma remove_code [code]:
   "Set.remove x (set xs) = set (removeAll x xs)"
   "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
-  by (simp_all add: remove_def Compl_insert)
+  by (simp_all add: set_eq_iff ac_simps)
 
 lemma filter_set [code]:
   "Set.filter P (set xs) = set (filter P xs)"