diff -r de51a86fc903 -r cc97b347b301 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Fri Jul 04 20:18:47 2014 +0200
@@ -830,11 +830,11 @@
       case 0 show ?case by simp
     next
       case (Suc m) thus ?case
-        by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
+        by (metis Suc_eq_plus1 assms add.commute add.left_commute subset_trans)
     qed
   }
   hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
-    by (metis add_commute le_add_diff_inverse nat_less_le)
+    by (metis add.commute le_add_diff_inverse nat_less_le)
   thus ?thesis
     by (auto simp add: disjoint_family_on_def)
       (metis insert_absorb insert_subset le_SucE le_antisym not_leE)