src/Pure/Thy/sessions.scala

   lazy val root_syntax =
     Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
       (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
       IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
 
-  private object Parser extends Parse.Parser
+  private object Parser extends Parse.Parser with Options.Parser
   {
     private abstract class Entry
     private sealed case class Chapter(name: String) extends Entry
     private sealed case class Session_Entry(
       pos: Position.T,

     private val session_entry: Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
 
       val option =
-        name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
+        option_name ~ opt($$$("=") ~! option_value ^^
+          { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
       val theories =
         ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
           ((options | success(Nil)) ~ rep(theory_xname)) ^^