diff -r 5004aca20821 -r 882091eb1e9a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -2495,8 +2495,8 @@
     next
       fix R
       show "rel_fn R =
-            (BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
-             BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
+            (BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
+             BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
         unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
         apply transfer
         unfolding rel_fun_def subset_iff image_iff