Added set comprehension as a syntactic abbreviation:
{e | x1..xn. P} means {u. ? x1 .. xn. u=e & P}

--- a/Set.thy	Wed Jun 01 13:24:54 1994 +0200
+++ b/Set.thy	Wed Jun 15 19:28:35 1994 +0200
@@ -44,7 +44,8 @@
 
   (** Binding Constants **)
 
-  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})") (*collection*)
+  "@Coll"       :: "[idt, bool] => 'a set"            ("(1{_./ _})")
+  "@SetCompr"   :: "['a, idts, bool] => 'a set"       ("{_ |/_./ _}")
 
   (* Big Intersection / Union *)
 
@@ -104,9 +105,44 @@
 
 end
 
+ML
 
-ML
+local
+
+(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *)
+
+fun dummyC(s) = Const(s,dummyT);
+
+val ex_tr = snd(mk_binder_tr("? ","Ex"));
+
+fun nvars(Const("_idts",_) $ _ $ idts) = nvars(idts)+1
+  | nvars(_) = 1;
+
+fun setcompr_tr[e,idts,b] =
+  let val eq = dummyC("op =") $ Bound(nvars(idts)) $ e
+      val P = dummyC("op &") $ eq $ b
+      val exP = ex_tr [idts,P]
+  in dummyC("Collect") $ Abs("",dummyT,exP) end;
+
+val ex_tr' = snd(mk_binder_tr' ("Ex","DUMMY"));
+
+fun setcompr_tr'[Abs(_,_,P)] =
+  let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
+        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ _) $ _, n) =
+            if n>0 andalso m=n then () else raise Match
+
+      fun tr'(_ $ abs) =
+        let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]
+        in dummyC("@SetCompr") $ e $ idts $ Q end
+  in ok(P,0); tr'(P) end;
+
+in
+
+val parse_translation = [("@SetCompr",setcompr_tr)];
+val print_translation = [("Collect",setcompr_tr')];
 
 val print_ast_translation =
   map HOL.alt_ast_tr' [("@Ball", "*Ball"), ("@Bex", "*Bex")];
 
+end;
+