diff -r d314a4e8038f -r 172aa230ce69 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Nov 27 21:53:38 2011 +0100
+++ b/src/HOL/Set.thy	Sun Nov 27 22:03:22 2011 +0100
@@ -1797,7 +1797,6 @@
 val bspec = @{thm bspec}
 val contra_subsetD = @{thm contra_subsetD}
 val distinct_lemma = @{thm distinct_lemma}
-val eq_to_mono = @{thm eq_to_mono}
 val equalityCE = @{thm equalityCE}
 val equalityD1 = @{thm equalityD1}
 val equalityD2 = @{thm equalityD2}