diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/ex/Hex_Bin_Examples.thy
--- a/src/HOL/ex/Hex_Bin_Examples.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/ex/Hex_Bin_Examples.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -25,7 +25,7 @@
 lemma "- 0x0A = - 10" by (rule refl)
 
 text \<open>
-  Hex and bin numerals are printed as decimal: @{term "0b10"}
+  Hex and bin numerals are printed as decimal: \<^term>\<open>0b10\<close>
 \<close>
 term "0b10"
 term "0x0A"