src/HOL/Probability/ex/Measure_Not_CCC.thy

     using pair_COCOUNT[of "SIGMA j:UNIV. {j}" POW] by auto
   have X_single: "\<And>x. x \<notin> J \<Longrightarrow> X = {x}"
     using eq[unfolded set_eq_iff] by force
   
   have "uncountable (UNIV - J)"
-    using `countable J` uncountable_UNIV_real uncountable_minus_countable by blast
+    using \<open>countable J\<close> uncountable_UNIV_real uncountable_minus_countable by blast
   then have "infinite (UNIV - J)"
     by (auto intro: countable_finite)
   then have "\<exists>A. finite A \<and> card A = 2 \<and> A \<subseteq> UNIV - J"
     by (rule infinite_arbitrarily_large)
   then obtain i j where ij: "i \<in> UNIV - J" "j \<in> UNIV - J" "i \<noteq> j"