1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 06 12:05:01 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 06 12:22:00 2013 +0200
     1.3 @@ -2656,7 +2656,6 @@
     1.4        using goal1(2) B
     1.5        apply auto
     1.6        done
     1.7 -      thm has_integralD[OF goal1(1) *]
     1.8      obtain g where g:
     1.9        "gauge g"
    1.10        "\<And>p. p tagged_division_of {a..b} \<Longrightarrow> g fine p \<Longrightarrow>