src/HOL/Analysis/Conformal_Mappings.thy

     proof -
       have [simp]: "p' \<notin> path_image g" "p' \<notin> path_image pg" "p'\<notin>path_image cp"
         using "2.prems"(8) that
         apply blast
         apply (metis Diff_iff Diff_insert2 contra_subsetD pg(4) that)
-        by (meson DiffD2 cp(4) set_rev_mp subset_insertI that)
+        by (meson DiffD2 cp(4) rev_subsetD subset_insertI that)
       have "winding_number g' p' = winding_number g p'
           + winding_number (pg +++ cp +++ reversepath pg) p'" unfolding g'_def
         apply (subst winding_number_join)
         apply (simp_all add: valid_path_imp_path)
         apply (intro not_in_path_image_join)