src/ZF/Induct/Multiset.thy

--- a/src/ZF/Induct/Multiset.thy	Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Sun Sep 29 21:57:47 2024 +0200
@@ -75,7 +75,8 @@
 
 syntax
   "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix MCollect\<close>\<close>{# _ \<in> _./ _#})\<close>)
-syntax_consts "_MColl" \<rightleftharpoons> MCollect
+syntax_consts
+  MCollect
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"