
diff -r fa5476c54731 -r 56247fdb8bbb src/Doc/Tutorial/ToyList/ToyList.thy
--- a/src/Doc/Tutorial/ToyList/ToyList.thy	Mon Dec 06 15:10:15 2021 +0100
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy	Mon Dec 06 15:34:54 2021 +0100
@@ -107,7 +107,7 @@
 When Isabelle prints a syntax error message, it refers to the HOL syntax as
 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}.
 
-Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}.
+Comments\index{comment} must be in enclosed in \texttt{(*}and\texttt{*)}.
 
 \section{Evaluation}
 \index{evaluation}




