src/HOL/Proofs/Extraction/Euclid.thy

--- a/src/HOL/Proofs/Extraction/Euclid.thy	Tue Mar 10 16:12:35 2015 +0000
+++ b/src/HOL/Proofs/Extraction/Euclid.thy	Mon Mar 16 15:30:00 2015 +0000
@@ -210,8 +210,8 @@
 
 lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
 proof -
-  let ?k = "fact n + 1"
-  have "1 < fact n + 1" by simp
+  let ?k = "fact n + (1::nat)"
+  have "1 < ?k" by simp
   then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover
   have "n < p"
   proof -