allow multiple 'keywords' as in 'fixes';
tuned comments;

--- a/src/Pure/Thy/thy_header.ML	Thu Mar 15 00:10:45 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 09:55:42 2012 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Thy/thy_header.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Theory headers -- independent of outer syntax.
+Static theory header information.
 *)
 
 signature THY_HEADER =
@@ -80,7 +80,10 @@
 val theory_name = Parse.group (fn () => "theory name") Parse.name;
 
 val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags);
-val keyword_decl = Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind);
+val keyword_decl =
+  Scan.repeat1 Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind) >>
+  (fn (names, kind) => map (rpair kind) names);
+val keyword_decls = Parse.and_list1 keyword_decl >> flat;
 
 val file =
   Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
@@ -91,7 +94,7 @@
 val args =
   theory_name --
   (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) --
-  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! (Parse.and_list1 keyword_decl)) [] --
+  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --
   Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --|
   Parse.$$$ beginN >>
   (fn (((name, imports), keywords), uses) => make name imports keywords uses);

--- a/src/Pure/Thy/thy_header.scala	Thu Mar 15 00:10:45 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 09:55:42 2012 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Thy/thy_header.scala
     Author:     Makarius
 
-Theory headers -- independent of outer syntax.
+Static theory header information.
 */
 
 package isabelle
@@ -51,11 +51,11 @@
     val keyword_kind =
       atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) }
     val keyword_decl =
-      name ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
-      { case x ~ y => (x, y) }
-    val keywords =
+      rep1(name) ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^
+      { case xs ~ y => xs.map((_, y)) }
+    val keyword_decls =
       keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
-      { case x ~ ys => x :: ys }
+      { case xs ~ yss => (xs :: yss).flatten }
 
     val file =
       keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
@@ -64,7 +64,7 @@
     val args =
       theory_name ~
       (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~
-      (opt(keyword(KEYWORDS) ~! keywords) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
+      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       keyword(BEGIN) ^^
       { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }