diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/Misc/pairs2.thy
--- a/src/Doc/Tutorial/Misc/pairs2.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/Misc/pairs2.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -20,7 +20,7 @@
 as a degenerate product with 0 components.
 \item
 Products, like type @{typ nat}, are datatypes, which means
-in particular that @{text induct_tac} and @{text case_tac} are applicable to
+in particular that \<open>induct_tac\<close> and \<open>case_tac\<close> are applicable to
 terms of product type.
 Both split the term into a number of variables corresponding to the tuple structure
 (up to 7 components).