diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -1568,7 +1568,7 @@
      (auto simp add: pmf.rel_map intro: pmf.rel_mono[THEN le_funD, THEN le_funD, THEN le_boolD, THEN mp, OF _ pq] fg)
 
 text \<open>
-  Proof that @{const rel_pmf} preserves orders.
+  Proof that \<^const>\<open>rel_pmf\<close> preserves orders.
   Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
   Theoretical Computer Science 12(1):19--37, 1980,
   \<^url>\<open>https://doi.org/10.1016/0304-3975(80)90003-1\<close>