diff -r 826a5fd4d36c -r 0230af0f3c59 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 30 19:29:06 2017 +0000
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Oct 31 07:11:03 2017 +0000
@@ -291,8 +291,8 @@
 next
   case False
   with assms show ?thesis
-    using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
-    by (auto simp add: residues_def gcd_int_def) force
+    using residues.euler_theorem [of "int m" "int a"] cong_int_iff
+    by (auto simp add: residues_def gcd_int_def) fastforce
 qed
 
 lemma fermat_theorem: