1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 27 09:15:26 2011 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 27 09:45:10 2011 +0100
     1.3 @@ -1814,7 +1814,7 @@
     1.4    unfolding monoidal_def forall_option neutral_lifted[OF assms] using monoidal_ac[OF assms] by auto
     1.5  
     1.6  definition "support opp f s = {x. x\<in>s \<and> f x \<noteq> neutral opp}"
     1.7 -definition "fold' opp e s \<equiv> (if finite s then fold opp e s else e)"
     1.8 +definition "fold' opp e s \<equiv> (if finite s then Finite_Set.fold opp e s else e)"
     1.9  definition "iterate opp s f \<equiv> fold' (\<lambda>x a. opp (f x) a) (neutral opp) (support opp f s)"
    1.10  
    1.11  lemma support_subset[intro]:"support opp f s \<subseteq> s" unfolding support_def by auto