diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Map.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -268,7 +268,7 @@
   using dom_map_option [of "\<lambda>_. g" m] by (simp add: comp_def)
 
 
-subsection \<open>@{const map_option} related\<close>
+subsection \<open>\<^const>\<open>map_option\<close> related\<close>
 
 lemma map_option_o_empty [simp]: "map_option f \<circ> empty = empty"
 by (rule ext) simp