src/HOL/Groups_Big.thy

--- a/src/HOL/Groups_Big.thy	Wed Oct 09 14:12:56 2024 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Oct 09 22:00:12 2024 +0200
@@ -1415,8 +1415,8 @@
 sublocale prod: comm_monoid_set times 1
   defines prod = prod.F and prod' = prod.G ..
 
-abbreviation Prod (\<open>(\<open>open_block notation=\<open>prefix \<Prod>\<close>\<close>\<Prod>_)\<close> [1000] 999)
-  where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
+abbreviation Prod (\<open>\<Prod>\<close>)
+  where "\<Prod> \<equiv> prod (\<lambda>x. x)"
 
 end