diff -r 713424d012fd -r 70076ba563d2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -91,10 +91,13 @@
   "\<lambda>a M b. if b = a then Suc (M b) else M b"
 by (rule add_mset_in_multiset)
 
+nonterminal multiset_args
 syntax
-  "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
+  "" :: "'a \<Rightarrow> multiset_args"  ("_")
+  "_multiset_args" :: "'a \<Rightarrow> multiset_args \<Rightarrow> multiset_args"  ("_,/ _")
+  "_multiset" :: "multiset_args \<Rightarrow> 'a multiset"    ("{#(_)#}")
 syntax_consts
-  "_multiset" == add_mset
+  "_multiset_args" "_multiset" == add_mset
 translations
   "{#x, xs#}" == "CONST add_mset x {#xs#}"
   "{#x#}" == "CONST add_mset x {#}"