diff -r 2d9cf954a829 -r cce82e360c2f src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 23 19:05:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Mar 23 19:05:14 2015 +0100
@@ -133,7 +133,7 @@
     apply (simp add: LIM_zero_iff [where l = D, symmetric])
     apply (simp add: Lim_within dist_norm)
     apply (simp add: nonzero_norm_divide [symmetric])
-    apply (simp add: 1 diff_add_eq_diff_diff ac_simps)
+    apply (simp add: 1 diff_diff_eq ac_simps)
     done
 qed
 
@@ -299,14 +299,14 @@
   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
     (\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm(y - x) < d \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> e * norm (y - x))"
   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
-    eventually_at dist_norm diff_add_eq_diff_diff
+    eventually_at dist_norm diff_diff_eq
   by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
 
 lemma has_derivative_within_alt2:
   "(f has_derivative f') (at x within s) \<longleftrightarrow> bounded_linear f' \<and>
     (\<forall>e>0. eventually (\<lambda>y. norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at x within s))"
   unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
-    eventually_at dist_norm diff_add_eq_diff_diff
+    eventually_at dist_norm diff_diff_eq
   by (force simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
 
 lemma has_derivative_at_alt: