diff -r e5f809f52f26 -r 9402a7f15ed5 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Oct 20 21:32:54 2014 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Oct 20 21:44:33 2014 +0200
@@ -194,8 +194,7 @@
 
   Note that the syntax of antiquotations may \emph{not} include source
   comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
-  text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
-  "*"}@{verbatim "}"}.
+  text @{verbatim "{*"}~@{text "\<dots>"}~@{verbatim "*}"}.
 
   \begin{description}