# HG changeset patch
# User huffman
# Date 1313611849 25200
# Node ID e37e1ef33bb8452a13b7a1a8b4855d1fc6c64c7d
# Parent  336dd390e4a4f1b5d1b518e55b36c5bf49c4f9db# Parent  45fb4b29c2679bb82e4a178043ff3424a9adaf77
merged

diff -r 336dd390e4a4 -r e37e1ef33bb8 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Wed Aug 17 13:10:11 2011 -0700
+++ b/src/HOL/Quotient.thy	Wed Aug 17 13:10:49 2011 -0700
@@ -643,10 +643,18 @@
     have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
     then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
     have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
-      by (metis Collect_def abs_inverse)
+    proof -
+      assume "R r r" and "R s s"
+      then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
+        by (metis abs_inverse)
+      also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
+        by rule simp_all
+      finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
+    qed
     then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
       using equivp[simplified part_equivp_def] by metis
     qed
+
 end
 
 subsection {* ML setup *}