diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/Advanced/WFrec.thy
--- a/src/Doc/Tutorial/Advanced/WFrec.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/Advanced/WFrec.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -5,7 +5,7 @@
 functions. Sometimes this can be inconvenient or
 impossible. Fortunately, \isacommand{recdef} supports much more
 general definitions. For example, termination of Ackermann's function
-can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
+can be shown by means of the \rmindex{lexicographic product} \<open><*lex*>\<close>:
 \<close>
 
 consts ack :: "nat\<times>nat \<Rightarrow> nat"
@@ -108,7 +108,7 @@
 (hints recdef_wf: wf_greater)
 
 text\<open>\noindent
-Alternatively, we could have given @{text "measure (\<lambda>k::nat. 10-k)"} for the
+Alternatively, we could have given \<open>measure (\<lambda>k::nat. 10-k)\<close> for the
 well-founded relation in our \isacommand{recdef}.  However, the arithmetic
 goal in the lemma above would have arisen instead in the \isacommand{recdef}
 termination proof, where we have less control.  A tailor-made termination