diff -r 8c3eec5812d8 -r ae44f16dcea5 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Feb 16 17:01:40 2016 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Feb 16 22:28:19 2016 +0100
@@ -2795,13 +2795,9 @@
         by (rule, transfer) (auto simp add: rel_fun_def)
     next
       fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
-      show "rel_fn R =
-            (BNF_Def.Grp {x. set_fn x \<subseteq> {(x, y). R x y}} (map_fn fst))\<inverse>\<inverse> OO
-             BNF_Def.Grp {x. set_fn x \<subseteq> {(x, y). R x y}} (map_fn snd)"
-        unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
-        apply transfer
-        unfolding rel_fun_def subset_iff image_iff
-        by auto (force, metis prod.collapse)
+      show "rel_fn R = (\<lambda>x y. \<exists>z. set_fn z \<subseteq> {(x, y). R x y} \<and> map_fn fst z = x \<and> map_fn snd z = y)"
+        unfolding fun_eq_iff relcompp.simps conversep.simps
+        by transfer (force simp: rel_fun_def subset_iff)
     qed
 
 text \<open> \blankline \<close>