--- a/src/HOL/Set.thy Sat Dec 30 22:37:07 2017 +0100
+++ b/src/HOL/Set.thy Sun Dec 31 21:42:20 2017 +0000
@@ -46,7 +46,7 @@
syntax (ASCII)
"_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/: _)./ _})")
syntax
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/\<in> _)./ _})")
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/ \<in> _)./ _})")
translations
"{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"