diff -r 8c3eec5812d8 -r ae44f16dcea5 src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Tue Feb 16 17:01:40 2016 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Tue Feb 16 22:28:19 2016 +0100
@@ -606,10 +606,9 @@
     unfolding rel_cset_alt_def[abs_def] by fast
 next
   fix R
-  show "rel_cset R =
-        (BNF_Def.Grp {x. rcset x \<subseteq> Collect (case_prod R)} (cimage fst))\<inverse>\<inverse> OO
-         BNF_Def.Grp {x. rcset x \<subseteq> Collect (case_prod R)} (cimage snd)"
-  unfolding rel_cset_alt_def[abs_def] rel_cset_aux by simp
+  show "rel_cset R = (\<lambda>x y. \<exists>z. rcset z \<subseteq> {(x, y). R x y} \<and>
+    cimage fst z = x \<and> cimage snd z = y)"
+  unfolding rel_cset_alt_def[abs_def] rel_cset_aux[unfolded OO_Grp_alt] by simp
 qed(simp add: bot_cset.rep_eq)
 
 end