src/HOL/Probability/Product_Measure.thy

 proof -
   interpret finite_product_sigma_finite M \<mu> "{}" by default (fact finite.emptyI)
   have "\<And>A. measure (Pi\<^isub>E {} A) = 1"
     using assms by (subst measure_times) auto
   then show ?thesis
-    unfolding positive_integral_alt simple_function_def simple_integral_def_raw
+    unfolding positive_integral_def simple_function_def simple_integral_def_raw
   proof (simp add: P_empty, intro antisym)
     show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> f}. f (\<lambda>k. undefined))"
       by (intro le_SUPI) auto
     show "(SUP f:{g. g \<le> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)"
       by (intro SUP_leI) (auto simp: le_fun_def)