diff -r e18ba60a1cf8 -r b58a575d211e src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Sun Mar 03 20:13:25 2019 +0100
+++ b/src/Pure/Isar/document_structure.scala	Sun Mar 03 20:27:42 2019 +0100
@@ -24,8 +24,7 @@
     command.span.is_kind(keywords,
       kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
 
-  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
-  {
+  def proper_heading_level(command: Command): Option[Int] =
     command.span.name match {
       case Thy_Header.CHAPTER => Some(0)
       case Thy_Header.SECTION => Some(1)
@@ -33,10 +32,12 @@
       case Thy_Header.SUBSUBSECTION => Some(3)
       case Thy_Header.PARAGRAPH => Some(4)
       case Thy_Header.SUBPARAGRAPH => Some(5)
-      case _ if is_theory_command(keywords, command) => Some(6)
       case _ => None
     }
-  }
+
+  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
+    proper_heading_level(command) orElse
+      (if (is_theory_command(keywords, command)) Some(6) else None)