--- a/src/HOL/Extraction/Euclid.thy	Mon Jun 28 15:32:13 2010 +0200
+++ b/src/HOL/Extraction/Euclid.thy	Mon Jun 28 15:32:17 2010 +0200
@@ -44,7 +44,7 @@
   done
 
 lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
-  by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps)
+  by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
 
 lemma not_prime_ex_mk:
   assumes n: "Suc 0 < n"