diff -r 274b4edca859 -r a4e82b58d833 src/HOL/Factorial.thy
--- a/src/HOL/Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
+++ b/src/HOL/Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
@@ -130,11 +130,11 @@
 lemma fact_ge_self: "fact n \<ge> n"
   by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
 
-lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::{semiring_div,linordered_semidom})"
+lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a::linordered_semidom)"
   by (induct m) (auto simp: le_Suc_eq)
 
-lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semiring_div,linordered_semidom}) = 0"
-  by (auto simp add: fact_dvd)
+lemma fact_mod: "m \<le> n \<Longrightarrow> fact n mod (fact m :: 'a::{semidom_modulo, linordered_semidom}) = 0"
+  by (simp add: mod_eq_0_iff_dvd fact_dvd)
 
 lemma fact_div_fact:
   assumes "m \<ge> n"