diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Mon Aug 08 14:13:14 2016 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Aug 08 17:47:51 2016 +0200
@@ -2250,7 +2250,7 @@
 
 subsection \<open>Irreducible Elements are Prime\<close>
 
-lemma (in factorial_monoid) irreducible_is_prime:
+lemma (in factorial_monoid) irreducible_prime:
   assumes pirr: "irreducible G p"
     and pcarr: "p \<in> carrier G"
   shows "prime G p"
@@ -2340,7 +2340,7 @@
 
 
 \<comment>"A version using @{const factors}, more complicated"
-lemma (in factorial_monoid) factors_irreducible_is_prime:
+lemma (in factorial_monoid) factors_irreducible_prime:
   assumes pirr: "irreducible G p"
     and pcarr: "p \<in> carrier G"
   shows "prime G p"
@@ -3638,7 +3638,7 @@
 done
 
 sublocale factorial_monoid \<subseteq> primeness_condition_monoid
-  by standard (rule irreducible_is_prime)
+  by standard (rule irreducible_prime)
 
 
 lemma (in factorial_monoid) primeness_condition: