diff -r 07a7544c0535 -r b65c4370f831 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -81,7 +81,8 @@
                               (option (pair (pair string (list string)) (list string)))))
                               (list YXML.string_of_body)))) a;
                         val imports' = map (rpair Position.none) imports;
-                        val header = Thy_Header.make (name, Position.none) imports' keywords;
+                        val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
+                        val header = Thy_Header.make (name, Position.none) imports' keywords';
                       in Document.Deps {master = master, header = header, errors = errors} end,
                     fn (a :: b, c) =>
                       Document.Perspective (bool_atom a, map int_atom b,