src/HOL/Probability/Finite_Product_Measure.thy

 proof -
   interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
   have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
     using assms by (subst measure_times) auto
   then show ?thesis
-    unfolding positive_integral_def simple_function_def simple_integral_def_raw
+    unfolding positive_integral_def simple_function_def simple_integral_def [abs_def]
   proof (simp add: P_empty, intro antisym)
     show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
       by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
     show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
       by (intro SUP_least) (auto simp: le_fun_def simp: max_def split: split_if_asm)