diff -r 8711db9f078a -r 858a225ebb62 src/HOL/ex/Sqrt_Script.thy
--- a/src/HOL/ex/Sqrt_Script.thy	Tue Aug 09 11:57:24 2016 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy	Tue Aug 09 12:30:31 2016 +0200
@@ -17,7 +17,7 @@
 subsection \<open>Preliminaries\<close>
 
 lemma prime_nonzero:  "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
-  by (force simp add: is_prime_nat_iff)
+  by (force simp add: prime_nat_iff)
 
 lemma prime_dvd_other_side:
     "(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
@@ -32,7 +32,7 @@
   apply (erule disjE)
    apply (frule mult_le_mono, assumption)
    apply auto
-  apply (force simp add: is_prime_nat_iff)
+  apply (force simp add: prime_nat_iff)
   done
 
 lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"