diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/Finite_Map.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -9,7 +9,7 @@
   abbrevs "(=" = "\<subseteq>\<^sub>f"
 begin
 
-subsection \<open>Auxiliary constants and lemmas over @{type map}\<close>
+subsection \<open>Auxiliary constants and lemmas over \<^type>\<open>map\<close>\<close>
 
 parametric_constant map_add_transfer[transfer_rule]: map_add_def
 parametric_constant map_of_transfer[transfer_rule]: map_of_def
@@ -1029,7 +1029,7 @@
 by transfer' (auto simp: set_of_map_def)
 
 
-subsection \<open>@{const size} setup\<close>
+subsection \<open>\<^const>\<open>size\<close> setup\<close>
 
 definition size_fmap :: "('a \<Rightarrow> nat) \<Rightarrow> ('b \<Rightarrow> nat) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> nat" where
 [simp]: "size_fmap f g m = size_fset (\<lambda>(a, b). f a + g b) (fset_of_fmap m)"
@@ -1060,7 +1060,7 @@
   done
 
 setup \<open>
-BNF_LFP_Size.register_size_global @{type_name fmap} @{const_name size_fmap}
+BNF_LFP_Size.register_size_global \<^type_name>\<open>fmap\<close> \<^const_name>\<open>size_fmap\<close>
   @{thm size_fmap_overloaded_def} @{thms size_fmap_def size_fmap_overloaded_simps}
   @{thms fmap_size_o_map}
 \<close>
@@ -1431,7 +1431,7 @@
   fmfilter fmadd fmmap fmmap_keys fmcomp
   checking SML Scala Haskell? OCaml?
 
-\<comment> \<open>\<open>lifting\<close> through @{type fmap}\<close>
+\<comment> \<open>\<open>lifting\<close> through \<^type>\<open>fmap\<close>\<close>
 
 experiment begin