src/HOL/Number_Theory/Gauss.thy

--- a/src/HOL/Number_Theory/Gauss.thy	Fri Feb 26 18:33:01 2016 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy	Fri Feb 26 22:15:09 2016 +0100
@@ -205,7 +205,7 @@
   by (simp add: cong_altdef_int) (metis gcd.commute prime_imp_coprime_int)
 
 lemma A_prod_relprime: "gcd (setprod id A) p = 1"
-  by (metis id_def all_A_relprime setprod_coprime_int)
+  by (metis id_def all_A_relprime setprod_coprime)
 
 
 subsection \<open>Relationships Between Gauss Sets\<close>