diff -r efb98d27dc1a -r cda018294515 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -19,10 +19,9 @@
   val all_current: theory -> bool
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
-  val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list ->
-    theory list -> theory
-  val load_thy: int -> Path.T -> string -> string list -> (Path.T * bool) list ->
-    Position.T -> string -> theory list -> theory * unit future
+  val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
+  val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
+    theory list -> theory * unit future
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
 end;
@@ -85,7 +84,9 @@
     val text = File.read master_file;
     val (name', imports, uses) =
       if name = Context.PureN then (Context.PureN, [], [])
-      else Thy_Header.read (Path.position master_file) text;
+      else
+        let val {name, imports, uses, ...} = Thy_Header.read (Path.position master_file) text
+        in (name, imports, uses) end;
     val _ = name <> name' andalso
       error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name');
   in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
@@ -159,21 +160,23 @@
 
 (* load_thy *)
 
-fun begin_theory dir name imports uses parents =
+fun begin_theory dir {name, imports, keywords, uses} parents =
   Theory.begin_theory name parents
   |> put_deps dir imports
+  |> fold Thy_Header.declare_keyword keywords
   |> fold (require o fst) uses
   |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   |> Theory.checkpoint;
 
-fun load_thy update_time dir name imports uses pos text parents =
+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 _ = Present.init_theory name;
     fun init () =
-      begin_theory dir name imports uses parents
+      begin_theory dir header parents
       |> Present.begin_theory update_time dir uses;
 
     val toks = Thy_Syntax.parse_tokens lexs pos text;