1.1 --- a/src/Pure/Isar/parse.scala	Thu Mar 15 14:13:49 2012 +0100
     1.2 +++ b/src/Pure/Isar/parse.scala	Thu Mar 15 14:22:54 2012 +0100
     1.3 @@ -53,6 +53,7 @@
     1.4        atom(Token.Kind.KEYWORD.toString + " " + quote(name),
     1.5          tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
     1.6  
     1.7 +    def string: Parser[String] = atom("string", _.is_string)
     1.8      def name: Parser[String] = atom("name declaration", _.is_name)
     1.9      def xname: Parser[String] = atom("name reference", _.is_xname)
    1.10      def text: Parser[String] = atom("text", _.is_text)

     2.1 --- a/src/Pure/Isar/token.scala	Thu Mar 15 14:13:49 2012 +0100
     2.2 +++ b/src/Pure/Isar/token.scala	Thu Mar 15 14:22:54 2012 +0100
     2.3 @@ -70,6 +70,7 @@
     2.4      kind == Token.Kind.ALT_STRING ||
     2.5      kind == Token.Kind.VERBATIM ||
     2.6      kind == Token.Kind.COMMENT
     2.7 +  def is_string: Boolean = kind == Token.Kind.STRING
     2.8    def is_name: Boolean =
     2.9      kind == Token.Kind.IDENT ||
    2.10      kind == Token.Kind.SYM_IDENT ||

     3.1 --- a/src/Pure/Thy/thy_header.ML	Thu Mar 15 14:13:49 2012 +0100
     3.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 14:22:54 2012 +0100
     3.3 @@ -81,7 +81,7 @@
     3.4  
     3.5  val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags);
     3.6  val keyword_decl =
     3.7 -  Scan.repeat1 Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >>
     3.8 +  Scan.repeat1 Parse.string -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >>
     3.9    (fn (names, kind) => map (rpair kind) names);
    3.10  val keyword_decls = Parse.and_list1 keyword_decl >> flat;
    3.11  

     4.1 --- a/src/Pure/Thy/thy_header.scala	Thu Mar 15 14:13:49 2012 +0100
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 14:22:54 2012 +0100
     4.3 @@ -51,7 +51,7 @@
     4.4      val keyword_kind =
     4.5        atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
     4.6      val keyword_decl =
     4.7 -      rep1(name) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
     4.8 +      rep1(string) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
     4.9        { case xs ~ y => xs.map((_, y)) }
    4.10      val keyword_decls =
    4.11        keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^