diff -r 85ed00c1fe7c -r 340738057c8c src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Fri Feb 19 13:40:50 2016 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Mon Feb 22 14:37:56 2016 +0000
@@ -1229,7 +1229,7 @@
     s: "\<And>i. simple_function M (s i)" and
     pointwise: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. s i x) \<longlonglongrightarrow> f x" and
     bound: "\<And>i x. x \<in> space M \<Longrightarrow> norm (s i x) \<le> 2 * norm (f x)"
-    by (simp add: norm_conv_dist) metis
+    by simp metis
   
   show ?thesis
   proof (rule integrableI_sequence)
@@ -2545,7 +2545,7 @@
   then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
     "\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) \<longlonglongrightarrow> f x y"
     "\<And>i x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> norm (s i (x, y)) \<le> 2 * norm (f x y)"
-    by (auto simp: space_pair_measure norm_conv_dist)
+    by (auto simp: space_pair_measure)
 
   have [measurable]: "\<And>i. s i \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
     by (rule borel_measurable_simple_function) fact