--- a/src/Doc/Sugar/Sugar.thy Fri Nov 06 21:49:02 2015 +0100
+++ b/src/Doc/Sugar/Sugar.thy Fri Nov 06 23:31:11 2015 +0100
@@ -137,7 +137,7 @@
suppresses question marks; variables that end in digits,
e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
e.g. @{text"x1.0"}, their internal index. This can be avoided by
-turning the last digit into a subscript: write \verb!x\<^sub>1! and
+turning the last digit into a subscript: write \<^verbatim>\<open>x\<^sub>1\<close> and
obtain the much nicer @{text"x\<^sub>1"}. *}
(*<*)declare [[show_question_marks = false]](*>*)