src/Doc/Tutorial/Misc/pairs2.thy

--- a/src/Doc/Tutorial/Misc/pairs2.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/Doc/Tutorial/Misc/pairs2.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -19,7 +19,7 @@
 element denoted by~\cdx{()}.  This type can be viewed
 as a degenerate product with 0 components.
 \item
-Products, like type @{typ nat}, are datatypes, which means
+Products, like type \<^typ>\<open>nat\<close>, are datatypes, which means
 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