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 \ 'a multiset" (\{#(\notation=\mixfix multiset enumeration\\_)#}\) + "_multiset" :: "args \ 'a multiset" (\(\indent=2 notation=\mixfix multiset enumeration\\{#_#})\) syntax_consts add_mset translations