diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/Bit.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -87,7 +87,7 @@
   by (simp_all add: equal set_iff)
 
 
-subsection \<open>Type @{typ bit} forms a field\<close>
+subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close>
 
 instantiation bit :: field
 begin
@@ -128,7 +128,7 @@
   unfolding plus_bit_def by (simp split: bit.split)
 
 
-subsection \<open>Numerals at type @{typ bit}\<close>
+subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close>
 
 text \<open>All numerals reduce to either 0 or 1.\<close>
 
@@ -145,7 +145,7 @@
   by (simp only: numeral_Bit1 bit_add_self add_0_left)
 
 
-subsection \<open>Conversion from @{typ bit}\<close>
+subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close>
 
 context zero_neq_one
 begin