extended set comprehension notation with {pttrn : A . P}

--- a/src/HOL/Product_Type.thy	Mon Mar 11 18:33:21 2013 +0100
+++ b/src/HOL/Product_Type.thy	Tue Mar 12 07:51:10 2013 +0100
@@ -184,6 +184,8 @@
 
 translations
   "(x, y)" == "CONST Pair x y"
+  "_pattern x y" => "CONST Pair x y"
+  "_patterns x y" => "CONST Pair x y"
   "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
   "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
   "%(x, y). b" == "CONST prod_case (%x y. b)"

--- a/src/HOL/Set.thy	Mon Mar 11 18:33:21 2013 +0100
+++ b/src/HOL/Set.thy	Tue Mar 12 07:51:10 2013 +0100
@@ -48,11 +48,11 @@
   "{x. P}" == "CONST Collect (%x. P)"
 
 syntax
-  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
+  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
 syntax (xsymbols)
-  "_Collect" :: "idt => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
+  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
 translations
-  "{x:A. P}" => "{x. x:A & P}"
+  "{p:A. P}" => "CONST Collect (%p. p:A & P)"
 
 lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
   by simp