diff -r 6040db6b929d -r e149e3e320a3 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Sep 21 20:33:44 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Sep 21 22:43:06 2016 +0200
@@ -329,20 +329,21 @@
   printing, notably spaces, blocks, and breaks. The general template format is
   a sequence over any of the following entities.
 
-  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence of characters other than
-  the following special characters:
-
-  \<^medskip>
-  \begin{tabular}{ll}
-    \<^verbatim>\<open>'\<close> & single quote \\
-    \<^verbatim>\<open>_\<close> & underscore \\
-    \<open>\<index>\<close> & index symbol \\
-    \<^verbatim>\<open>(\<close> & open parenthesis \\
-    \<^verbatim>\<open>)\<close> & close parenthesis \\
-    \<^verbatim>\<open>/\<close> & slash \\
-    \<open>\<open> \<close>\<close> & cartouche delimiters \\
-  \end{tabular}
-  \<^medskip>
+  \<^descr> \<open>d\<close> is a delimiter, namely a non-empty sequence delimiter items of the
+  following form:
+    \<^enum> a control symbol followed by a cartouche
+    \<^enum> a single symbol, excluding the following special characters:
+      \<^medskip>
+      \begin{tabular}{ll}
+        \<^verbatim>\<open>'\<close> & single quote \\
+        \<^verbatim>\<open>_\<close> & underscore \\
+        \<open>\<index>\<close> & index symbol \\
+        \<^verbatim>\<open>(\<close> & open parenthesis \\
+        \<^verbatim>\<open>)\<close> & close parenthesis \\
+        \<^verbatim>\<open>/\<close> & slash \\
+        \<open>\<open> \<close>\<close> & cartouche delimiters \\
+      \end{tabular}
+      \<^medskip>
 
   \<^descr> \<^verbatim>\<open>'\<close> escapes the special meaning of these meta-characters, producing a
   literal version of the following character, unless that is a blank.