# HG changeset patch
# User nipkow
# Date 1235292748 -3600
# Node ID 46c88406e6c031aaaf76b970ef025894453de2ee
# Parent  f9182081d6c68a4c501f84947c944594ab790465
name fix

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