src/HOL/Number_Theory/Residues.thy

   also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p"
     apply (rule prod_cong)
     apply auto
     done
   also have "\<dots> = fact (p - 1) mod p"
-    apply (subst fact_altdef_nat)
+    apply (simp add: fact_setprod)
     apply (insert assms)
     apply (subst res_prime_units_eq)
     apply (simp add: int_setprod zmod_int setprod_int_eq)
     done
   finally have "fact (p - 1) mod p = \<ominus> \<one>" .

   assumes "prime p"
   shows "[fact (p - 1) = - 1] (mod p)"
 proof (cases "p = 2")
   case True
   then show ?thesis
-    by (simp add: cong_int_def fact_altdef_nat)
+    by (simp add: cong_int_def fact_setprod)
 next
   case False
   then show ?thesis
     using assms prime_ge_2_nat
     by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq)