diff -r bda7527ccf05 -r cc2d676d5395 src/Doc/Tutorial/Recdef/Nested1.thy
--- a/src/Doc/Tutorial/Recdef/Nested1.thy	Wed Dec 26 16:07:28 2018 +0100
+++ b/src/Doc/Tutorial/Recdef/Nested1.thy	Wed Dec 26 16:25:20 2018 +0100
@@ -23,9 +23,9 @@
 unproved termination condition
 @{prop[display]"t : set ts --> size t < Suc (size_term_list ts)"}
 where @{term set} returns the set of elements of a list
-and @{text"size_term_list :: term list \<Rightarrow> nat"} is an auxiliary
+and \<open>size_term_list :: term list \<Rightarrow> nat\<close> is an auxiliary
 function automatically defined by Isabelle
-(while processing the declaration of @{text term}).  Why does the
+(while processing the declaration of \<open>term\<close>).  Why does the
 recursive call of @{const trev} lead to this
 condition?  Because \isacommand{recdef} knows that @{term map}
 will apply @{const trev} only to elements of @{term ts}. Thus the