src/Pure/Thy/thy_load.ML
changeset 46958 0ec8f04e753a
parent 46938 cda018294515
child 46959 cdc791910460
--- 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 =