diff -r ab8310c0e6d9 -r 6fe9cdf547c4 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed May 17 09:00:04 2023 +0200
+++ b/src/HOL/Library/FSet.thy	Fri May 26 09:48:55 2023 +0200
@@ -171,10 +171,10 @@
   "{|x|}"     == "CONST finsert x {||}"
 
 abbreviation fmember :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) where
-  "a |\<in>| A \<equiv> a \<in> fset A"
+  "x |\<in>| X \<equiv> x \<in> fset X"
 
 abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
-  "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
+  "x |\<notin>| X \<equiv> x \<notin> fset X"
 
 context includes lifting_syntax
 begin