uniform heading commands work in any context, even in theory header;
discontinued obsolete 'sect', 'subsect', 'subsubsect';
marked obsolete 'header' as legacy;

--- a/NEWS	Sun Nov 02 13:26:20 2014 +0100
+++ b/NEWS	Sun Nov 02 15:27:37 2014 +0100
@@ -167,6 +167,13 @@
 
 *** Document preparation ***
 
+* Document headings work uniformly via the commands 'chapter',
+'section', 'subsection', 'subsubsection' -- in any context, even
+before the initial 'theory' command.  Obsolete proof commands 'sect',
+'subsect', 'subsubsect' have been discontinued.  The Obsolete 'header'
+command is still retained for some time, but should be replaced by
+'chapter', 'section' etc. Minor INCOMPATIBILITY.
+
 * Official support for "tt" style variants, via \isatt{...} or
 \begin{isabellett}...\end{isabellett}. The somewhat fragile \verb or
 verbatim environment of LaTeX is no longer used. This allows @{ML} etc.

--- a/lib/texinputs/isabelle.sty	Sun Nov 02 13:26:20 2014 +0100
+++ b/lib/texinputs/isabelle.sty	Sun Nov 02 15:27:37 2014 +0100
@@ -127,9 +127,6 @@
 \newcommand{\isamarkupsection}[1]{\section{#1}}
 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
-\newcommand{\isamarkupsect}[1]{\section{#1}}
-\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
-\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
 
 \newif\ifisamarkup
 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}

--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Nov 02 15:27:37 2014 +0100
@@ -22,16 +22,12 @@
 
 text \<open>
   \begin{matharray}{rcl}
-    @{command_def "header"} & : & @{text "toplevel \<rightarrow> toplevel"} \\[0.5ex]
-    @{command_def "chapter"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
-    @{command_def "section"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
-    @{command_def "subsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
-    @{command_def "subsubsection"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "chapter"} & : & @{text "any \<rightarrow> any"} \\
+    @{command_def "section"} & : & @{text "any \<rightarrow> any"} \\
+    @{command_def "subsection"} & : & @{text "any \<rightarrow> any"} \\
+    @{command_def "subsubsection"} & : & @{text "any \<rightarrow> any"} \\
     @{command_def "text"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "text_raw"} & : & @{text "local_theory \<rightarrow> local_theory"} \\[0.5ex]
-    @{command_def "sect"} & : & @{text "proof \<rightarrow> proof"} \\
-    @{command_def "subsect"} & : & @{text "proof \<rightarrow> proof"} \\
-    @{command_def "subsubsect"} & : & @{text "proof \<rightarrow> proof"} \\
     @{command_def "txt"} & : & @{text "proof \<rightarrow> proof"} \\
     @{command_def "txt_raw"} & : & @{text "proof \<rightarrow> proof"} \\
   \end{matharray}
@@ -51,26 +47,17 @@
     (@@{command chapter} | @@{command section} | @@{command subsection} |
       @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text}
     ;
-    (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} |
-      @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text}
+    (@@{command text_raw} | @@{command txt} | @@{command txt_raw}) @{syntax text}
   \<close>}
 
   \begin{description}
 
-  \item @{command header} provides plain text markup just preceding
-  the formal beginning of a theory.  The corresponding {\LaTeX} macro
-  is @{verbatim \<open>\isamarkupheader\<close>}, which acts like @{command
-  section} by default.
-  
-  \item @{command chapter}, @{command section}, @{command subsection},
-  and @{command subsubsection} mark chapter and section headings
-  within the main theory body or local theory targets.  The
-  corresponding {\LaTeX} macros are @{verbatim \<open>\isamarkupchapter\<close>},
-  @{verbatim \<open>\isamarkupsection\<close>}, @{verbatim \<open>\isamarkupsubsection\<close>} etc.
-
-  \item @{command sect}, @{command subsect}, and @{command subsubsect}
-  mark section headings within proofs.  The corresponding {\LaTeX}
-  macros are @{verbatim \<open>\isamarkupsect\<close>}, @{verbatim \<open>\isamarkupsubsect\<close>} etc.
+  \item @{command chapter}, @{command section}, @{command subsection}, and
+  @{command subsubsection} mark chapter and section headings within the
+  theory source; this works in any context, even before the initial
+  @{command theory} command. The corresponding {\LaTeX} macros are
+  @{verbatim \<open>\isamarkupchapter\<close>}, @{verbatim \<open>\isamarkupsection\<close>},
+  @{verbatim \<open>\isamarkupsubsection\<close>}, @{verbatim \<open>\isamarkupsubsubsection\<close>}.
 
   \item @{command text} and @{command txt} specify paragraphs of plain
   text.  This corresponds to a {\LaTeX} environment @{verbatim
@@ -91,8 +78,7 @@
 
   \medskip The proof markup commands closely resemble those for theory
   specifications, but have a different formal status and produce
-  different {\LaTeX} macros.  The default definitions coincide for
-  analogous commands such as @{command section} and @{command sect}.
+  different {\LaTeX} macros.
 \<close>
 
 

--- a/src/Doc/Tutorial/Documents/Documents.thy	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Sun Nov 02 15:27:37 2014 +0100
@@ -424,24 +424,6 @@
   do not affect the formal meaning of a theory (or proof), but result
   in corresponding {\LaTeX} elements.
 
-  There are separate markup commands depending on the textual context:
-  in header position (just before \isakeyword{theory}), within the
-  theory body, or within a proof.  The header needs to be treated
-  specially here, since ordinary theory and proof commands may only
-  occur \emph{after} the initial \isakeyword{theory} specification.
-
-  \medskip
-
-  \begin{tabular}{llll}
-  header & theory & proof & default meaning \\\hline
-    & \commdx{chapter} & & \verb,\chapter, \\
-  \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
-    & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
-    & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
-  \end{tabular}
-
-  \medskip
-
   From the Isabelle perspective, each markup command takes a single
   $text$ argument (delimited by \verb,",~@{text \<dots>}~\verb,", or
   \verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,},).  After stripping any

--- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 15:27:37 2014 +0100
@@ -48,10 +48,11 @@
   val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
   val print_type: (string list * (string * string option)) ->
     Toplevel.transition -> Toplevel.transition
-  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
-  val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.source) ->
+  val local_theory_markup: (xstring * Position.T) option * Symbol_Pos.source ->
     Toplevel.transition -> Toplevel.transition
   val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
+  val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
+    Toplevel.transition -> Toplevel.transition
 end;
 
 structure Isar_Cmd: ISAR_CMD =
@@ -377,11 +378,21 @@
 
 (* markup commands *)
 
-fun header_markup txt = Toplevel.keep (fn state =>
-  if Toplevel.is_toplevel state then Thy_Output.check_text txt state
-  else raise Toplevel.UNDEF);
-
 fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (Thy_Output.check_text txt);
 val proof_markup = Toplevel.present_proof o Thy_Output.check_text;
 
+fun reject_target NONE = ()
+  | reject_target (SOME (_, pos)) =
+      error ("Illegal target specification -- not a theory context" ^ Position.here pos);
+
+fun heading_markup (loc, txt) =
+  Toplevel.keep (fn state =>
+    if Toplevel.is_toplevel state then
+     (legacy_feature "Obsolete 'header' command -- use 'chapter', 'section' etc. instead";
+      reject_target loc;
+      Thy_Output.check_text txt state)
+    else raise Toplevel.UNDEF) o
+  local_theory_markup (loc, txt) o
+  Toplevel.present_proof (fn state => (reject_target loc; Thy_Output.check_text txt state));
+
 end;

--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 02 15:27:37 2014 +0100
@@ -12,27 +12,27 @@
 val _ =
   Outer_Syntax.markup_command Thy_Output.Markup
     @{command_spec "header"} "theory header"
-    (Parse.document_source >> Isar_Cmd.header_markup);
+    (Parse.document_source >> (fn s => Isar_Cmd.heading_markup (NONE, s)));
 
 val _ =
   Outer_Syntax.markup_command Thy_Output.Markup
     @{command_spec "chapter"} "chapter heading"
-    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
+    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
 
 val _ =
   Outer_Syntax.markup_command Thy_Output.Markup
     @{command_spec "section"} "section heading"
-    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
+    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
 
 val _ =
   Outer_Syntax.markup_command Thy_Output.Markup
     @{command_spec "subsection"} "subsection heading"
-    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
+    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
 
 val _ =
   Outer_Syntax.markup_command Thy_Output.Markup
     @{command_spec "subsubsection"} "subsubsection heading"
-    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
+    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.heading_markup);
 
 val _ =
   Outer_Syntax.markup_command Thy_Output.MarkupEnv
@@ -45,21 +45,6 @@
     (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
 
 val _ =
-  Outer_Syntax.markup_command Thy_Output.Markup
-    @{command_spec "sect"} "formal comment (proof)"
-    (Parse.document_source >> Isar_Cmd.proof_markup);
-
-val _ =
-  Outer_Syntax.markup_command Thy_Output.Markup
-    @{command_spec "subsect"} "formal comment (proof)"
-    (Parse.document_source >> Isar_Cmd.proof_markup);
-
-val _ =
-  Outer_Syntax.markup_command Thy_Output.Markup
-    @{command_spec "subsubsect"} "formal comment (proof)"
-    (Parse.document_source >> Isar_Cmd.proof_markup);
-
-val _ =
   Outer_Syntax.markup_command Thy_Output.MarkupEnv
     @{command_spec "txt"} "formal comment (proof)"
     (Parse.document_source >> Isar_Cmd.proof_markup);

--- a/src/Pure/Isar/keyword.ML	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Sun Nov 02 15:27:37 2014 +0100
@@ -10,12 +10,9 @@
   val kind_of: T -> string
   val kind_files_of: T -> string * string list
   val diag: T
+  val heading: T
   val thy_begin: T
   val thy_end: T
-  val thy_heading1: T
-  val thy_heading2: T
-  val thy_heading3: T
-  val thy_heading4: T
   val thy_decl: T
   val thy_decl_block: T
   val thy_load: T
@@ -25,9 +22,6 @@
   val qed_script: T
   val qed_block: T
   val qed_global: T
-  val prf_heading2: T
-  val prf_heading3: T
-  val prf_heading4: T
   val prf_goal: T
   val prf_block: T
   val prf_open: T
@@ -90,12 +84,9 @@
 (* kinds *)
 
 val diag = kind "diag";
+val heading = kind "heading";
 val thy_begin = kind "thy_begin";
 val thy_end = kind "thy_end";
-val thy_heading1 = kind "thy_heading1";
-val thy_heading2 = kind "thy_heading2";
-val thy_heading3 = kind "thy_heading3";
-val thy_heading4 = kind "thy_heading4";
 val thy_decl = kind "thy_decl";
 val thy_decl_block = kind "thy_decl_block";
 val thy_load = kind "thy_load";
@@ -105,9 +96,6 @@
 val qed_script = kind "qed_script";
 val qed_block = kind "qed_block";
 val qed_global = kind "qed_global";
-val prf_heading2 = kind "prf_heading2";
-val prf_heading3 = kind "prf_heading3";
-val prf_heading4 = kind "prf_heading4";
 val prf_goal = kind "prf_goal";
 val prf_block = kind "prf_block";
 val prf_open = kind "prf_open";
@@ -120,10 +108,9 @@
 val prf_script = kind "prf_script";
 
 val kinds =
-  [diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global,
-    prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
-    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
+    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 
 (* tags *)
@@ -235,30 +222,25 @@
 
 val is_diag = command_category [diag];
 
-val is_heading =
-  command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    prf_heading2, prf_heading3, prf_heading4];
+val is_heading = command_category [heading];
 
 val is_theory_begin = command_category [thy_begin];
 
 val is_theory_load = command_category [thy_load];
 
 val is_theory = command_category
-  [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_decl_block, thy_goal];
+  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal];
 
 val is_theory_body = command_category
-  [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_decl_block, thy_goal];
+  [thy_load, thy_decl, thy_decl_block, thy_goal];
 
 val is_proof = command_category
-  [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
-    prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
-    prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+  [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_proof_body = command_category
-  [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open, prf_close, prf_chain,
-    prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+  [diag, heading, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm,
+    prf_asm_goal, prf_asm_goal_script, prf_script];
 
 val is_theory_goal = command_category [thy_goal];
 val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];

--- a/src/Pure/Isar/keyword.scala	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Sun Nov 02 15:27:37 2014 +0100
@@ -13,12 +13,9 @@
 
   val MINOR = "minor"
   val DIAG = "diag"
+  val HEADING = "heading"
   val THY_BEGIN = "thy_begin"
   val THY_END = "thy_end"
-  val THY_HEADING1 = "thy_heading1"
-  val THY_HEADING2 = "thy_heading2"
-  val THY_HEADING3 = "thy_heading3"
-  val THY_HEADING4 = "thy_heading4"
   val THY_DECL = "thy_decl"
   val THY_DECL_BLOCK = "thy_decl_block"
   val THY_LOAD = "thy_load"
@@ -27,9 +24,6 @@
   val QED_SCRIPT = "qed_script"
   val QED_BLOCK = "qed_block"
   val QED_GLOBAL = "qed_global"
-  val PRF_HEADING2 = "prf_heading2"
-  val PRF_HEADING3 = "prf_heading3"
-  val PRF_HEADING4 = "prf_heading4"
   val PRF_GOAL = "prf_goal"
   val PRF_BLOCK = "prf_block"
   val PRF_OPEN = "prf_open"
@@ -46,26 +40,21 @@
 
   val diag = Set(DIAG)
 
-  val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
-    PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
+  val heading = Set(HEADING)
 
-  val theory =
-    Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
-      THY_LOAD, THY_DECL, THY_GOAL)
+  val theory = Set(THY_BEGIN, THY_END, THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
 
   val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
 
-  val theory_body =
-    Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL)
+  val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
 
   val proof =
-    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
-      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL,
-      PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
+      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
 
   val proof_body =
-    Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN,
-      PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+    Set(DIAG, HEADING, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM,
+      PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
 
   val theory_goal = Set(THY_GOAL)
   val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)

--- a/src/Pure/Isar/outer_syntax.scala	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Sun Nov 02 15:27:37 2014 +0100
@@ -277,14 +277,16 @@
 
   def heading_level(command: Command): Option[Int] =
   {
-    keyword_kind(command.name) match {
-      case _ if command.name == "header" => Some(0)
-      case Some(Keyword.THY_HEADING1) => Some(1)
-      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
-      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
-      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
-      case Some(kind) if Keyword.theory(kind) => Some(5)
-      case _ => None
+    command.name match {
+      case "chapter" => Some(0)
+      case "section" | "header" => Some(1)
+      case "subsection" => Some(2)
+      case "subsubsection" => Some(3)
+      case _ =>
+        keyword_kind(command.name) match {
+          case Some(kind) if Keyword.theory(kind) => Some(4)
+          case _ => None
+        }
     }
   }
 

--- a/src/Pure/Pure.thy	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/Pure.thy	Sun Nov 02 15:27:37 2014 +0100
@@ -14,15 +14,12 @@
     "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
   and "theory" :: thy_begin % "theory"
-  and "header" :: diag
-  and "chapter" :: thy_heading1
-  and "section" :: thy_heading2
-  and "subsection" :: thy_heading3
-  and "subsubsection" :: thy_heading4
+  and "header" :: heading
+  and "chapter" :: heading
+  and "section" :: heading
+  and "subsection" :: heading
+  and "subsubsection" :: heading
   and "text" "text_raw" :: thy_decl
-  and "sect" :: prf_heading2 % "proof"
-  and "subsect" :: prf_heading3 % "proof"
-  and "subsubsect" :: prf_heading4 % "proof"
   and "txt" "txt_raw" :: prf_decl % "proof"
   and "default_sort" :: thy_decl == ""
   and "typedecl" "type_synonym" "nonterminal" "judgment"

--- a/src/Pure/System/options.scala	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/System/options.scala	Sun Nov 02 15:27:37 2014 +0100
@@ -76,7 +76,7 @@
 
   lazy val options_syntax =
     Outer_Syntax.init() + ":" + "=" + "--" +
-      (SECTION, Keyword.THY_HEADING2) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
+      (SECTION, Keyword.HEADING) + (PUBLIC, Keyword.THY_DECL) + (OPTION, Keyword.THY_DECL)
 
   lazy val prefs_syntax = Outer_Syntax.init() + "="
 

--- a/src/Pure/Thy/thy_header.ML	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sun Nov 02 15:27:37 2014 +0100
@@ -67,6 +67,11 @@
 (* header keywords *)
 
 val headerN = "header";
+val chapterN = "chapter";
+val sectionN = "section";
+val subsectionN = "subsection";
+val subsubsectionN = "subsubsection";
+
 val theoryN = "theory";
 val importsN = "imports";
 val keywordsN = "keywords";
@@ -75,7 +80,7 @@
 val header_lexicons =
   pairself (Scan.make_lexicon o map Symbol.explode)
    (["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN],
-    [headerN, theoryN]);
+    [headerN, chapterN, sectionN, subsectionN, subsubsectionN, theoryN]);
 
 
 (* header args *)
@@ -118,10 +123,16 @@
 
 (* read header *)
 
+val heading =
+  (Parse.command_name headerN ||
+    Parse.command_name chapterN ||
+    Parse.command_name sectionN ||
+    Parse.command_name subsectionN ||
+    Parse.command_name subsubsectionN) --
+  Parse.tags -- Parse.!!! Parse.document_source;
+
 val header =
-  (Parse.command_name headerN -- Parse.tags) |--
-    (Parse.!!! (Parse.document_source -- (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
-  (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
+  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
 
 fun token_source pos str =
   str

--- a/src/Pure/Thy/thy_header.scala	Sun Nov 02 13:26:20 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 02 15:27:37 2014 +0100
@@ -16,6 +16,11 @@
 object Thy_Header extends Parse.Parser
 {
   val HEADER = "header"
+  val CHAPTER = "chapter"
+  val SECTION = "section"
+  val SUBSECTION = "subsection"
+  val SUBSUBSECTION = "subsubsection"
+
   val THEORY = "theory"
   val IMPORTS = "imports"
   val KEYWORDS = "keywords"
@@ -23,8 +28,8 @@
   val BEGIN = "begin"
 
   private val lexicon =
-    Scan.Lexicon("%", "(", ")", ",", "::", "==",
-      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY)
+    Scan.Lexicon("%", "(", ")", ",", "::", "==", AND, BEGIN,
+      HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY)
 
 
   /* theory file name */
@@ -74,9 +79,15 @@
       keyword(BEGIN) ^^
       { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
 
-    (keyword(HEADER) ~ tags) ~!
-      ((document_source ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
-    (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
+    val heading =
+      (keyword(HEADER) |
+        keyword(CHAPTER) |
+        keyword(SECTION) |
+        keyword(SUBSECTION) |
+        keyword(SUBSUBSECTION)) ~
+      tags ~! document_source
+
+    (rep(heading) ~ keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   }