diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Retracts.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -604,7 +604,7 @@
       show "continuous_on W (\<lambda>x. if x \<in> W - V then a else h (j x, g x))"
         apply (subst Weq)
         apply (rule continuous_on_cases_local)
-            apply (simp_all add: Weq [symmetric] WWV continuous_on_const *)
+            apply (simp_all add: Weq [symmetric] WWV *)
           using WV' closedin_diff apply fastforce
          apply (auto simp: j0 j1)
         done
@@ -1408,7 +1408,7 @@
   proof (intro exI conjI)
     show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then x else r x)"
       apply (rule continuous_on_cases_local [OF clS clT])
-      using r by (auto simp: continuous_on_id)
+      using r by (auto)
   qed (use r in auto)
   also have "\<dots> retract_of U"
     by (rule Un)
@@ -2136,7 +2136,7 @@
   proof
     have "continuous_on (T \<union> (S - T)) ?g"
       apply (rule continuous_on_cases_local)
-      using Seq clo ope by (auto simp: contf continuous_on_const intro: continuous_on_cases_local)
+      using Seq clo ope by (auto simp: contf intro: continuous_on_cases_local)
     with Seq show "continuous_on S ?g"
       by metis
     show "?g ` S \<subseteq> U"