
diff -r 15261d78d7b5 -r eebb8270b3cc src/Doc/Sugar/Sugar.thy
--- 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.




