# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1514756540 0
# Node ID 54e2111d6f0ef8f7570ade4b981ca771a1ae1465
# Parent  897344e33c26cb8614b442dd0ca4832f4e692d6f
Restored correct spacing for set comprehensions

diff -r 897344e33c26 -r 54e2111d6f0e src/HOL/Set.thy
--- 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)"