diff -r 965769fe2b63 -r fc1556774cfe src/HOL/Probability/ex/Measure_Not_CCC.thy
--- a/src/HOL/Probability/ex/Measure_Not_CCC.thy	Mon Dec 07 16:48:10 2015 +0000
+++ b/src/HOL/Probability/ex/Measure_Not_CCC.thy	Mon Dec 07 20:19:59 2015 +0100
@@ -150,7 +150,7 @@
     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"