--- a/src/Doc/Sugar/Sugar.thy Fri Feb 07 21:27:11 2025 +0100
+++ b/src/Doc/Sugar/Sugar.thy Sat Feb 08 11:18:30 2025 +0100
@@ -533,9 +533,9 @@
You have to place the following lines before and after the snippet, where snippets must always be
consecutive lines of theory text:
\begin{quote}
-\verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\
+\verb!\text_raw\!\verb!<open>\snip{!\emph{snippetname}\verb!}{1}{2}{%\!\verb!<close>!\\
\emph{theory text}\\
-\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}!
+\verb!\text_raw\!\verb!<open>%endsnip\!\verb!<close>!
\end{quote}
where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1}
and \texttt{2} are explained in a moment.