diff -r c64628dbac00 -r ff12606337e9 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1211,7 +1211,7 @@
       apply (rule arg_cong[of _ _ interior])
       using p(8) uv by auto
     also have "\<dots> = {}"
-      unfolding interior_inter
+      unfolding interior_Int
       apply (rule inter_interior_unions_intervals)
       using p(6) p(7)[OF p(2)] p(3)
       apply auto
@@ -4872,7 +4872,7 @@
             "cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
           have "(cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<subseteq> cbox m n \<inter> cbox u v"
             by blast
-          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_inter[of "cbox m n"]]
+          note interior_mono[OF this, unfolded division_ofD(5)[OF p'' as(1-3)] interior_Int[of "cbox m n"]]
           then have "interior (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
             unfolding as Int_absorb by auto
           then show "content (cbox m n \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
@@ -7341,7 +7341,7 @@
               guess v' using pa[OF k(2)] .. note v' = conjunctD2[OF this] let ?v = "min v v'"
               have "box a ?v \<subseteq> k \<inter> k'"
                 unfolding v v' by (auto simp add: mem_box)
-              note interior_mono[OF this,unfolded interior_inter]
+              note interior_mono[OF this,unfolded interior_Int]
               moreover have "(a + ?v)/2 \<in> box a ?v"
                 using k(3-)
                 unfolding v v' content_eq_0 not_le
@@ -7372,7 +7372,7 @@
               let ?v = "max v v'"
               have "box ?v b \<subseteq> k \<inter> k'"
                 unfolding v v' by (auto simp: mem_box)
-                note interior_mono[OF this,unfolded interior_inter]
+                note interior_mono[OF this,unfolded interior_Int]
               moreover have " ((b + ?v)/2) \<in> box ?v b"
                 using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
               ultimately have " ((b + ?v)/2) \<in> interior k \<inter> interior k'"
@@ -8014,7 +8014,7 @@
     apply (rule assms(1)[unfolded connected_clopen,rule_format])
     apply rule
     defer
-    apply (rule continuous_closed_in_preimage[OF assms(4) closed_singleton])
+    apply (rule continuous_closedin_preimage[OF assms(4) closed_singleton])
     apply (rule open_openin_trans[OF assms(2)])
     unfolding open_contains_ball
   proof safe
@@ -9427,7 +9427,7 @@
     note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]]
     from this(2)[OF as(4,1)] guess u v by (elim exE) note uv=this
     have *: "interior (k \<inter> l) = {}"
-      unfolding interior_inter
+      unfolding interior_Int
       apply (rule q')
       using as
       unfolding r_def
@@ -10771,7 +10771,7 @@
           proof goal_cases
             case prems: (1 l y)
             have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
-              apply (subst(2) interior_inter)
+              apply (subst(2) interior_Int)
               apply (rule Int_greatest)
               defer
               apply (subst prems(4))
@@ -10960,7 +10960,7 @@
             from d'(4)[OF this(1)] d'(4)[OF this(2)]
             guess u1 v1 u2 v2 by (elim exE) note uv=this
             have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
-              apply (subst interior_inter)
+              apply (subst interior_Int)
               using d'(5)[OF prems(1-3)]
               apply auto
               done