diff -r de51a86fc903 -r cc97b347b301 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -614,7 +614,7 @@
     using f by (intro simple_function_partition) auto
   also have "\<dots> = c * integral\<^sup>S M f"
     using f unfolding simple_integral_def
-    by (subst setsum_ereal_right_distrib) (auto simp: emeasure_nonneg mult_assoc Int_def conj_commute)
+    by (subst setsum_ereal_right_distrib) (auto simp: emeasure_nonneg mult.assoc Int_def conj_commute)
   finally show ?thesis .
 qed
 
@@ -1129,7 +1129,7 @@
 lemma nn_integral_multc:
   assumes "f \<in> borel_measurable M" "0 \<le> c"
   shows "(\<integral>\<^sup>+ x. f x * c \<partial>M) = integral\<^sup>N M f * c"
-  unfolding mult_commute[of _ c] nn_integral_cmult[OF assms] by simp
+  unfolding mult.commute[of _ c] nn_integral_cmult[OF assms] by simp
 
 lemma nn_integral_indicator[simp]:
   "A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x. indicator A x\<partial>M) = (emeasure M) A"