diff -r 8e398d9bedf3 -r ed416f4ac34e src/HOL/BNF/BNF_GFP.thy
--- a/src/HOL/BNF/BNF_GFP.thy	Sat Jul 27 22:44:04 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Sun Jul 28 12:59:59 2013 +0200
@@ -106,15 +106,9 @@
 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
 unfolding fun_eq_iff by auto
 
-lemmas conversep_in_rel_Id_on =
-  trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]
-
 lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
 unfolding fun_eq_iff by auto
 
-lemmas relcompp_in_rel_Id_on =
-  trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]
-
 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
 unfolding Gr_def Grp_def fun_eq_iff by auto