diff -r bfc2e92d9b4c -r 261d42f0bfac src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Tue Oct 18 07:04:08 2016 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Oct 17 15:20:06 2016 +0200
@@ -10,7 +10,7 @@
 
 subsection\<open>Lemmas about previously defined terms\<close>
 
-lemma prime: 
+lemma prime_nat_iff'':
   "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
   unfolding prime_nat_iff
 proof safe
@@ -78,7 +78,7 @@
   from pa have ap: "coprime a p"
     by (metis gcd.commute) 
   have px:"coprime x p"
-    by (metis gcd.commute p prime x0 xp)
+    by (metis gcd.commute p prime_nat_iff'' x0 xp)
   obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
     by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
   {assume y0: "y = 0"