# HG changeset patch
# User wenzelm
# Date 1224189865 -7200
# Node ID ac1da69fbc5a63f09c6273c1c6f1463d083609b4
# Parent  4c8fa015ec7f16ab1bccf8e50d1614490d065134
avoid accidental dependency of automated proof on sort equiv;

diff -r 4c8fa015ec7f -r ac1da69fbc5a 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