diff -r 5b67ac48b384 -r a40be2f10ca9 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Mar 15 09:55:42 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 10:16:21 2012 +0100
@@ -113,7 +113,7 @@
 
 sealed case class Thy_Header(
   name: String, imports: List[String],
-  keywords: List[(String, Option[(String, List[String])])],
+  keywords: List[Outer_Syntax.Decl],
   uses: List[(String, Boolean)])
 {
   def map(f: String => String): Thy_Header =