diff -r 94aa7b81bcf6 -r d0181abdbdac src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 15 22:08:53 2012 +0100
@@ -215,7 +215,8 @@
           val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
           val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
           val header' =
-            (List.app Keyword.declare keywords; header)
+            (List.app (fn (name, decl) =>
+                Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
               handle exn as ERROR _ => Exn.Exn exn;
           val nodes1 = nodes
             |> default_node name