src/HOL/Analysis/Tagged_Division.thy

     show "interior S \<inter> interior m = {}" if "m \<in> r1 - p" for m 
     proof -
       have "interior m \<inter> interior (\<Union>p) = {}"
       proof (rule Int_interior_Union_intervals)
         show "\<And>T. T\<in>p \<Longrightarrow> interior m \<inter> interior T = {}"
-          by (metis DiffD1 DiffD2 that r1(1) r1(7) set_rev_mp)
+          by (metis DiffD1 DiffD2 that r1(1) r1(7) rev_subsetD)
       qed (use divp in auto)
       then show "interior S \<inter> interior m = {}"
         unfolding divp by auto
     qed 
   qed (use r1 in auto)