--- 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