1.1 --- a/src/HOL/Quotient.thy	Tue Aug 16 07:56:17 2011 -0700
     1.2 +++ b/src/HOL/Quotient.thy	Tue Aug 16 19:47:50 2011 +0200
     1.3 @@ -643,10 +643,18 @@
     1.4      have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
     1.5      then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
     1.6      have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
     1.7 -      by (metis Collect_def abs_inverse)
     1.8 +    proof -
     1.9 +      assume "R r r" and "R s s"
    1.10 +      then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
    1.11 +        by (metis abs_inverse)
    1.12 +      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))"
    1.13 +        by rule simp_all
    1.14 +      finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
    1.15 +    qed
    1.16      then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
    1.17        using equivp[simplified part_equivp_def] by metis
    1.18      qed
    1.19 +
    1.20  end
    1.21  
    1.22  subsection {* ML setup *}