
diff -r 8042869c2072 -r 843dba3d307a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 23:32:26 2024 +0200
@@ -92,7 +92,7 @@
 by (rule add_mset_in_multiset)
 
 syntax
-  "_multiset" :: "args \<Rightarrow> 'a multiset"    (\<open>{#(\<open>notation=\<open>mixfix multiset enumeration\<close>\<close>_)#}\<close>)
+  "_multiset" :: "args \<Rightarrow> 'a multiset"  (\<open>(\<open>indent=2 notation=\<open>mixfix multiset enumeration\<close>\<close>{#_#})\<close>)
 syntax_consts
   add_mset
 translations




