--- a/src/HOL/Relation.thy Thu Mar 22 18:37:20 2012 +0100
+++ b/src/HOL/Relation.thy Thu Mar 22 18:54:39 2012 +0100
@@ -543,7 +543,7 @@
"{} O R = {}"
by blast
-lemma prod_comp_bot1 [simp]:
+lemma pred_comp_bot1 [simp]:
"\<bottom> OO R = \<bottom>"
by (fact rel_comp_empty1 [to_pred])