diff -r a8b1a44d8264 -r 79f9fbef9106 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Mon Jan 12 16:45:35 2004 +0100
+++ b/src/HOL/Library/Primes.thy	Mon Jan 12 16:51:45 2004 +0100
@@ -200,7 +200,7 @@
   by (auto dest: prime_dvd_mult)
 
 lemma prime_dvd_power_two: "p \<in> prime ==> p dvd m\<twosuperior> ==> p dvd m"
-  by (rule prime_dvd_square) (simp_all add: power_two)
+  by (rule prime_dvd_square) (simp_all add: power2_eq_square)
 
 
 text {* \medskip Addition laws *}