diff -r e16649b70107 -r 8e46cea6a45a src/Pure/Tools/update_header.scala
--- a/src/Pure/Tools/update_header.scala	Sat Oct 17 20:27:12 2015 +0200
+++ b/src/Pure/Tools/update_header.scala	Sat Oct 17 21:15:10 2015 +0200
@@ -25,15 +25,19 @@
 
   /* command line entry point */
 
+  private val headings =
+    Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
+
   def main(args: Array[String])
   {
     Command_Line.tool0 {
       args.toList match {
         case section :: files =>
-          if (!Set("chapter", "section", "subsection", "subsubsection").contains(section))
+          if (!headings.contains(section))
             error("Bad heading command: " + quote(section))
           files.foreach(file => update_header(section, Path.explode(file)))
-        case _ => error("Bad arguments:\n" + cat_lines(args))
+        case _ =>
+            error("Bad arguments:\n" + cat_lines(args))
       }
     }
   }