1.1 --- a/src/HOL/Multivariate_Analysis/Gauge_Measure.thy	Thu Aug 26 21:03:14 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Gauge_Measure.thy	Fri Aug 27 10:55:20 2010 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4    shows "(\<Union> f) has_gmeasure (setsum m f)" using assms
     1.5  proof induct case (insert x s)
     1.6    have *:"(x \<inter> \<Union>s) = \<Union>{x \<inter> y| y. y\<in>s}"by auto
     1.7 -  show ?case unfolding Union_insert ring_class.setsum.insert[OF insert(1-2)] 
     1.8 +  show ?case unfolding Union_insert setsum.insert [OF insert(1-2)] 
     1.9      apply(rule has_gmeasure_negligible_union) unfolding *
    1.10      apply(rule insert) defer apply(rule insert) apply(rule insert) defer
    1.11      apply(rule insert) prefer 4 apply(rule negligible_unions)