diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Infinite_Product_Measure.thy
--- 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 "\ = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\ i \ 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 "\ \ 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) \ sigma_sets ?O ?M"