diff -r bbed46f40cf5 -r a82df75b7f85 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jan 10 15:57:55 2018 +0100
+++ b/src/HOL/Set.thy	Wed Jan 10 18:18:34 2018 +0100
@@ -20,20 +20,16 @@
     and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
 
 notation
-  member  ("'(\<in>')") and
-  member  ("(_/ \<in> _)" [51, 51] 50)
+  member  (infix "\<in>" 50)
 
 abbreviation not_member
   where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
 notation
-  not_member  ("'(\<notin>')") and
-  not_member  ("(_/ \<notin> _)" [51, 51] 50)
+  not_member  (infix "\<notin>" 50)
 
 notation (ASCII)
-  member  ("'(:')") and
-  member  ("(_/ : _)" [51, 51] 50) and
-  not_member  ("'(~:')") and
-  not_member  ("(_/ ~: _)" [51, 51] 50)
+  member  (infix ":" 50) and
+  not_member  (infix "~:" 50)
 
 
 text \<open>Set comprehensions\<close>