src/HOL/Topological_Spaces.thy

   obtain sb where sb: "sb \<in> S" "B \<inter> sb \<noteq> {}"
     using Blap by auto
   obtain x where x: "\<And>s. s \<in> S \<Longrightarrow> x \<in> s"
     using ne by auto
   then have "x \<in> \<Union>S"
-    using `sa \<in> S` by blast
+    using \<open>sa \<in> S\<close> by blast
   then have "x \<in> A \<or> x \<in> B"
     using cover by auto
   then show False
     using cs [unfolded connected_def]
     by (metis A B IntI Sup_upper sa sb disjs x cover empty_iff subset_trans)