diff -r 55b2afc5ddfc -r bdc2c6b40bf2 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jul 05 10:09:01 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sat Jul 05 11:01:53 2014 +0200
@@ -1578,7 +1578,7 @@
     have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
       using `bilinear h` by (rule bilinear_bounded)
     then show "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
-      by (simp add: mult_ac)
+      by (simp add: ac_simps)
   qed
 next
   assume "bounded_bilinear h"
@@ -1597,7 +1597,7 @@
     using bh [unfolded bilinear_conv_bounded_bilinear]
     by (rule bounded_bilinear.pos_bounded)
   then show ?thesis
-    by (simp only: mult_ac)
+    by (simp only: ac_simps)
 qed