define keywords early when processing the theory header, before running the body commands;

--- a/src/Pure/Isar/isar_syn.ML	Fri Mar 16 11:26:55 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 16 13:05:30 2012 +0100
@@ -9,11 +9,8 @@
 
 (** keywords **)
 
-(*keep keywords consistent with the parsers, otherwise be prepared for
-  unexpected errors*)
-
 val _ = Context.>> (Context.map_theory
-  (fold (fn name => Thy_Header.declare_keyword (name, NONE))
+  (fold (fn name => (Keyword.define (name, NONE); Thy_Header.declare_keyword (name, NONE)))
    ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
     "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
     "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",

--- a/src/Pure/Isar/keyword.ML	Fri Mar 16 11:26:55 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 13:05:30 2012 +0100
@@ -45,7 +45,7 @@
   val dest: unit -> string list * string list
   val keyword_statusN: string
   val status: unit -> unit
-  val declare: string -> T option -> unit
+  val define: string * T option -> unit
   val is_diag: string -> bool
   val is_control: string -> bool
   val is_regular: string -> bool
@@ -214,15 +214,15 @@
   in () end;
 
 
-(* declare *)
+(* define *)
 
-fun declare name NONE =
+fun define (name, NONE) =
      (change_keywords (fn ((minor, major), commands) =>
         let
           val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
         in ((minor', major), commands) end);
       keyword_status name)
-  | declare name (SOME kind) =
+  | define (name, SOME kind) =
      (change_keywords (fn ((minor, major), commands) =>
         let
           val major' = Scan.extend_lexicon (Symbol.explode name) major;

--- a/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 11:26:55 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Mar 16 13:05:30 2012 +0100
@@ -131,7 +131,7 @@
           if k = SOME kind then ()
           else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
       | NONE =>
-          if Context.theory_name thy = Context.PureN then Keyword.declare name (SOME kind)
+          if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind)
           else error ("Undeclared outer syntax command " ^ quote name));
   in
     Unsynchronized.change global_outer_syntax (map_commands (fn commands =>

--- a/src/Pure/PIDE/document.ML	Fri Mar 16 11:26:55 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Mar 16 13:05:30 2012 +0100
@@ -213,10 +213,8 @@
     | Header header =>
         let
           val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
-          val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
           val header' =
-            (List.app (fn (name, decl) =>
-                Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
+            ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
               handle exn as ERROR _ => Exn.Exn exn;
           val nodes1 = nodes
             |> default_node name

--- a/src/Pure/Thy/thy_header.ML	Fri Mar 16 11:26:55 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML	Fri Mar 16 13:05:30 2012 +0100
@@ -12,6 +12,7 @@
     uses: (Path.T * bool) list}
   val make: string -> string list -> (string * (string * string list) option) list ->
     (Path.T * bool) list -> header
+  val define_keywords: header -> unit
   val declare_keyword: string * (string * string list) option -> theory -> theory
   val the_keyword: theory -> string -> Keyword.T option
   val args: header parser
@@ -33,6 +34,9 @@
 
 (** keyword declarations **)
 
+fun define_keywords ({keywords, ...}: header) =
+  List.app (fn (name, decl) => Keyword.define (name, Option.map Keyword.make decl)) keywords;
+
 fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
 
 structure Data = Theory_Data
@@ -44,9 +48,7 @@
 );
 
 fun declare_keyword (name, decl) = Data.map (fn data =>
-  let
-    val kind = Option.map Keyword.make decl;
-    val _ = Keyword.declare name kind;
+  let val kind = Option.map Keyword.make decl
   in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
 
 fun the_keyword thy name =

--- a/src/Pure/Thy/thy_info.ML	Fri Mar 16 11:26:55 2012 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Mar 16 13:05:30 2012 +0100
@@ -314,6 +314,7 @@
     val {name, imports, ...} = header;
     val _ = kill_thy name;
     val _ = use_thys_wrt dir imports;
+    val _ = Thy_Header.define_keywords header;
     val parents = map (get_theory o base_name) imports;
   in Thy_Load.begin_theory dir header parents end;
 

--- a/src/Pure/Thy/thy_load.ML	Fri Mar 16 11:26:55 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Mar 16 13:05:30 2012 +0100
@@ -170,15 +170,17 @@
 
 fun load_thy update_time dir header pos text parents =
   let
-    val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
     val time = ! Toplevel.timing;
 
     val {name, imports, uses, ...} = header;
+    val _ = Thy_Header.define_keywords header;
     val _ = Present.init_theory name;
     fun init () =
       begin_theory dir header parents
       |> Present.begin_theory update_time dir uses;
 
+    val (lexs, outer_syntax) = Outer_Syntax.get_syntax ();
+
     val toks = Thy_Syntax.parse_tokens lexs pos text;
     val spans = Thy_Syntax.parse_spans toks;
     val elements =

--- a/src/Pure/Thy/thy_output.ML	Fri Mar 16 11:26:55 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Mar 16 13:05:30 2012 +0100
@@ -626,7 +626,7 @@
 
 (* embedded lemma *)
 
-val _ = Keyword.declare "by" NONE;  (*overlap with command category*)
+val _ = Keyword.define ("by", NONE);  (*overlap with command category*)
 
 val _ =
   Context.>> (Context.map_theory