diff -r e9ab4ad7bd15 -r 23307fd33906 src/Doc/Tutorial/Misc/appendix.thy
--- a/src/Doc/Tutorial/Misc/appendix.thy	Thu Jan 11 13:48:17 2018 +0100
+++ b/src/Doc/Tutorial/Misc/appendix.thy	Fri Jan 12 14:08:53 2018 +0100
@@ -2,7 +2,7 @@
 imports Main
 begin(*>*)
 
-text{*
+text\<open>
 \begin{table}[htbp]
 \begin{center}
 \begin{tabular}{lll}
@@ -28,6 +28,6 @@
 \label{tab:overloading}
 \end{center}
 \end{table}
-*}
+\<close>
 
 (*<*)end(*>*)