src/HOL/Analysis/Continuous_Extension.thy

           apply (rule continuous_intros *)+
           using ss_pos apply force
           done
       qed
       moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x
-        using nonneg [of x] by (simp add: F_def field_split_simps setdist_pos_le)
+        using nonneg [of x] by (simp add: F_def field_split_simps)
       ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)"
         by metis
     next
       show "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
         by (simp add: setdist_eq_0_sing_1 closure_def F_def)

   next
     case False
     show ?thesis
     proof (cases "T = U")
       case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
-        by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
+        by (rule_tac f = "\<lambda>x. b" in that) (auto)
     next
       case False
       with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T"
         by fastforce
       obtain f where f: "continuous_on U f"

   show ?thesis
   proof (cases "T = {}")
     case True show ?thesis
     proof (cases "S = U")
       case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
-        by (rule_tac f = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
+        by (rule_tac f = "\<lambda>x. a" in that) (auto)
     next
       case False
       with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
         by fastforce
       obtain f where f: "continuous_on U f"

           "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
           "\<And>x. x \<in> S \<Longrightarrow> f x = a"
           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
 proof (cases "a = b")
   case True then show ?thesis
-    by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
+    by (rule_tac f = "\<lambda>x. b" in that) (auto)
 next
   case False
   then show ?thesis
     apply (rule Urysohn_local_strong [OF assms])
     apply (erule that, assumption)