src/HOL/Old_Number_Theory/EulerFermat.thy

    apply (simp only: zcong_def)
    apply (subgoal_tac "zgcd a m = m")
     prefer 2
     apply (subst zdvd_iff_zgcd [symmetric])
      apply (rule_tac [4] zgcd_zcong_zgcd)
-       apply (simp_all add: zcong_sym)
+       apply (simp_all (no_asm_use) add: zcong_sym)
   done
 
 
 text {* \medskip @{term noXRRset} *}