--- a/src/HOL/Binomial.thy Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Binomial.thy Wed Feb 17 21:51:56 2016 +0100
@@ -1323,7 +1323,7 @@
also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
apply (subst div_mult_div_if_dvd [symmetric])
apply (auto simp add: algebra_simps)
- apply (metis fact_fact_dvd_fact dvd.order.trans nat_mult_dvd_cancel_disj)
+ apply (metis fact_fact_dvd_fact dvd_trans nat_mult_dvd_cancel_disj)
done
also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
apply (subst div_mult_div_if_dvd)