diff -r be0a4a0bf7f5 -r 4b40b8196dc7 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Doc/Implementation/ML.thy	Fri Aug 05 16:30:53 2016 +0200
@@ -70,11 +70,14 @@
   prose description of the purpose of the module. The latter can range from a
   single line to several paragraphs of explanations.
 
-  The rest of the file is divided into sections, subsections, subsubsections,
-  paragraphs etc.\ using a simple layout via ML comments as follows.
+  The rest of the file is divided into chapters, sections, subsections,
+  subsubsections, paragraphs etc.\ using a simple layout via ML comments as
+  follows.
 
   @{verbatim [display]
-\<open>  (*** section ***)
+\<open>  (**** chapter ****)
+ 
+  (*** section ***)
 
   (** subsection **)