src/Pure/System/build.scala

   private val THEORIES = "theories"
   private val FILES = "files"
 
   lazy val root_syntax =
     Outer_Syntax.init() + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-      SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
+      (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
 
   private object Parser extends Parse.Parser
   {
     def session_entry(pos: Position.T): Parser[Session_Entry] =
     {

 
       val theories =
         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
           { case _ ~ (x ~ y) => (x, y) }
 
-      ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
+      ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
         (keyword("!") ^^^ true | success(false)) ~
         (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
         (opt(keyword(IN) ~! path ^^ { case _ ~ x => x })) ~
         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~