diff -r be8c0e039a5e -r bc936d3d8b45 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -75,9 +75,9 @@
 
 syntax
   "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>)
+syntax_consts "_MColl" \<rightleftharpoons> MCollect
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
-syntax_consts "_MColl" \<rightleftharpoons> MCollect
 
   (* multiset orderings *)