diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -91,13 +91,10 @@
   "\<lambda>a M b. if b = a then Suc (M b) else M b"
 by (rule add_mset_in_multiset)
 
-nonterminal multiset_args
 syntax
-  "" :: "'a \<Rightarrow> multiset_args"  (\<open>_\<close>)
-  "_multiset_args" :: "'a \<Rightarrow> multiset_args \<Rightarrow> multiset_args"  (\<open>_,/ _\<close>)
-  "_multiset" :: "multiset_args \<Rightarrow> 'a multiset"    (\<open>{#(_)#}\<close>)
+  "_multiset" :: "args \<Rightarrow> 'a multiset"    (\<open>{#(\<open>notation=\<open>mixfix multiset enumeration\<close>\<close>_)#}\<close>)
 syntax_consts
-  "_multiset_args" "_multiset" == add_mset
+  add_mset
 translations
   "{#x, xs#}" == "CONST add_mset x {#xs#}"
   "{#x#}" == "CONST add_mset x {#}"