diff -r 8c3eec5812d8 -r ae44f16dcea5 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 16 17:01:40 2016 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Feb 16 22:28:19 2016 +0100
@@ -1097,10 +1097,9 @@
     finally show ?thesis .
   qed
 
-  show "\<And>R. rel_pmf R =
-         (BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO
-         BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)"
-     by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps)
+  show "\<And>R. rel_pmf R = (\<lambda>x y. \<exists>z. set_pmf z \<subseteq> {(x, y). R x y} \<and>
+    map_pmf fst z = x \<and> map_pmf snd z = y)"
+     by (auto simp add: fun_eq_iff rel_pmf.simps)
 
   show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
     for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"