--- a/src/HOL/MacLaurin.thy Wed Oct 09 23:00:52 2019 +0200
+++ b/src/HOL/MacLaurin.thy Wed Oct 09 14:51:54 2019 +0000
@@ -57,7 +57,7 @@
by (rule nonzero_divide_eq_eq[THEN iffD2]) auto
moreover
have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))"
- using \<open>0 < n - m\<close> by (simp add: divide_simps fact_reduce)
+ using \<open>0 < n - m\<close> by (simp add: field_split_simps fact_reduce)
ultimately show "DERIV (difg m) t :> difg (Suc m) t"
unfolding difg_def by (simp add: mult.commute)
qed