src/HOL/Number_Theory/Totient.thy

--- a/src/HOL/Number_Theory/Totient.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/Number_Theory/Totient.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -78,7 +78,7 @@
 qed (auto simp: totatives_def)
 
 lemma totatives_prime: "prime p \<Longrightarrow> totatives p = {0<..<p}"
-  using totatives_prime_power_Suc[of p 0] by fastforce
+  using totatives_prime_power_Suc [of p 0] by auto
 
 lemma bij_betw_totatives:
   assumes "m1 > 1" "m2 > 1" "coprime m1 m2"