diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Aug 08 14:13:14 2016 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Aug 08 17:47:51 2016 +0200
@@ -411,7 +411,7 @@
   interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor
     by standard (rule lcm_gcd_eucl_facts; assumption)+
   fix p assume p: "irreducible p"
-  thus "is_prime_elem p" by (rule irreducible_imp_prime_gcd)
+  thus "prime_elem p" by (rule irreducible_imp_prime_elem_gcd)
 qed
 
 lemma gcd_eucl_eq_gcd_factorial: "gcd_eucl = gcd_factorial"