
diff -r cc57255bf6ae -r 61171cbeedde src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Aug 13 23:45:29 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Aug 14 12:26:09 2016 +0200
@@ -1027,9 +1027,9 @@
 by (rule filter_preserves_multiset)
 
 syntax (ASCII)
-  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
+  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{#_ :# _./ _#})")
 syntax
-  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
+  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{#_ \<in># _./ _#})")
 translations
   "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
 




