src/HOL/ex/PER.thy

--- a/src/HOL/ex/PER.thy	Thu Oct 16 22:44:24 2008 +0200
+++ b/src/HOL/ex/PER.thy	Thu Oct 16 22:44:25 2008 +0200
@@ -223,7 +223,7 @@
 qed
 
 lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
-  using eqv_class_eqI eqv_class_eqD' by blast
+  using eqv_class_eqI eqv_class_eqD' by (blast del: eqv_refl)
 
 lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"
   using eqv_class_eqI eqv_class_eqD by blast