--- a/src/HOL/Real/ex/Sqrt_Irrational.thy	Mon Oct 22 11:01:30 2001 +0200
+++ b/src/HOL/Real/ex/Sqrt_Irrational.thy	Mon Oct 22 11:54:22 2001 +0200
@@ -119,7 +119,7 @@
   {
     fix m :: nat assume dvd: "m dvd 2"
     hence "m \<le> 2" by (simp add: dvd_imp_le)
-    moreover from dvd have "m \<noteq> 0" by (auto dest: dvd_0_left iff del: neq0_conv)
+    moreover from dvd have "m \<noteq> 0" by (auto iff del: neq0_conv)
     ultimately have "m = 1 \<or> m = 2" by arith
   }
   thus "2 \<in> prime" by (simp add: prime_def)