diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Set.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -38,15 +38,6 @@
   not_member  (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
 end
 
-bundle no_member_ASCII_syntax
-begin
-no_notation (ASCII)
-  member  (\<open>'(:')\<close>) and
-  member  (\<open>(\<open>notation=\<open>infix :\<close>\<close>_/ : _)\<close> [51, 51] 50) and
-  not_member  (\<open>'(~:')\<close>) and
-  not_member  (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
-end
-
 
 text \<open>Set comprehensions\<close>