1.1 --- a/src/HOL/Extraction/Euclid.thy Sat Feb 21 21:00:50 2009 +0100
1.2 +++ b/src/HOL/Extraction/Euclid.thy Sun Feb 22 09:52:28 2009 +0100
1.3 @@ -189,7 +189,7 @@
1.4 assume pn: "p \<le> n"
1.5 from `prime p` have "0 < p" by (rule prime_g_zero)
1.6 then have "p dvd n!" using pn by (rule dvd_factorial)
1.7 - with dvd have "p dvd ?k - n!" by (rule dvd_diff)
1.8 + with dvd have "p dvd ?k - n!" by (rule nat_dvd_diff)
1.9 then have "p dvd 1" by simp
1.10 with prime show False using prime_nd_one by auto
1.11 qed