diff -r 143d2514347f -r 6fe61da4c467 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Dec 17 12:51:30 2011 +0100
+++ b/src/HOL/Set.thy	Sat Dec 17 13:08:03 2011 +0100
@@ -1560,9 +1560,6 @@
 lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
   by blast
 
-lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
-  by iprover
-
 lemma ball_simps [simp, no_atp]:
   "\<And>A P Q. (\<forall>x\<in>A. P x \<or> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<or> Q)"
   "\<And>A P Q. (\<forall>x\<in>A. P \<or> Q x) \<longleftrightarrow> (P \<or> (\<forall>x\<in>A. Q x))"
@@ -1796,7 +1793,6 @@
 val bex_triv = @{thm bex_triv}
 val bspec = @{thm bspec}
 val contra_subsetD = @{thm contra_subsetD}
-val distinct_lemma = @{thm distinct_lemma}
 val equalityCE = @{thm equalityCE}
 val equalityD1 = @{thm equalityD1}
 val equalityD2 = @{thm equalityD2}