# HG changeset patch
# User wenzelm
# Date 1414943980 -3600
# Node ID ab1c65b015c35f14f0c42f373015ebd162d9911f
# Parent  7172c7ffb04788dedfd7be011f43d066f9768aa9
clarified legacy command;

diff -r 7172c7ffb047 -r ab1c65b015c3 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 16:54:06 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 02 16:59:40 2014 +0100
@@ -51,6 +51,7 @@
   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 header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
   val heading_markup: (xstring * Position.T) option * Symbol_Pos.source ->
     Toplevel.transition -> Toplevel.transition
 end;
@@ -385,12 +386,16 @@
   | reject_target (SOME (_, pos)) =
       error ("Illegal target specification -- not a theory context" ^ Position.here pos);
 
-fun heading_markup (loc, txt) =
+fun header_markup 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);
+
+fun heading_markup (loc, txt) =
+  Toplevel.keep (fn state =>
+    if Toplevel.is_toplevel state then (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));
diff -r 7172c7ffb047 -r ab1c65b015c3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Nov 02 16:54:06 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 02 16:59:40 2014 +0100
@@ -12,7 +12,7 @@
 val _ =
   Outer_Syntax.markup_command Thy_Output.Markup
     @{command_spec "header"} "theory header"
-    (Parse.document_source >> (fn s => Isar_Cmd.heading_markup (NONE, s)));
+    (Parse.document_source >> Isar_Cmd.header_markup);
 
 val _ =
   Outer_Syntax.markup_command Thy_Output.Markup