1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 12:51:52 2012 +0100
     1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 13:31:26 2012 +0100
     1.3 @@ -858,7 +858,7 @@
     1.4  using assms proof induct
     1.5    case empty
     1.6    interpret finite_product_sigma_finite M "{}" by default auto
     1.7 -  then show ?case by simp
     1.8 +  show ?case by simp
     1.9  next
    1.10    case (insert i I)
    1.11    note `finite I`[intro, simp]