--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 16:56:56 2012 +0100
@@ -874,7 +874,7 @@
by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
using J M.sets_into_space
- by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
+ by (auto simp: emb_def [abs_def] intro!: sigma_sets_vimage[symmetric]) blast
also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
using J by (intro sigma_sets_mono') auto
finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"