src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Tue Aug 07 12:35:24 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Aug 07 13:21:29 2012 +0200
@@ -107,12 +107,17 @@
     try { read(reader).map(Standard_System.decode_permissive_utf8) }
     finally { reader.close }
   }
+
+
+  /* keywords */
+
+  type Keywords = List[(String, Option[(String, List[String])])]
 }
 
 
 sealed case class Thy_Header(
   name: String, imports: List[String],
-  keywords: List[Outer_Syntax.Decl],
+  keywords: Thy_Header.Keywords,
   uses: List[(String, Boolean)])
 {
   def map(f: String => String): Thy_Header =