--- a/src/HOL/Lattices.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Lattices.thy Fri Jan 04 23:22:53 2019 +0100
@@ -802,7 +802,7 @@
qed
-subsection \<open>Lattice on @{typ bool}\<close>
+subsection \<open>Lattice on \<^typ>\<open>bool\<close>\<close>
instantiation bool :: boolean_algebra
begin
@@ -829,7 +829,7 @@
by auto
-subsection \<open>Lattice on @{typ "_ \<Rightarrow> _"}\<close>
+subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close>
instantiation "fun" :: (type, semilattice_sup) semilattice_sup
begin