--- a/src/HOL/Equiv_Relations.thy Mon Aug 15 22:31:17 2011 +0200
+++ b/src/HOL/Equiv_Relations.thy Tue Aug 16 07:17:15 2011 +0900
@@ -402,8 +402,8 @@
by (erule part_equivpE, erule transpE)
lemma part_equivp_typedef:
- "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
- by (auto elim: part_equivpE simp add: mem_def)
+ "part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}"
+ by (auto elim: part_equivpE)
text {* Total equivalences *}