src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Apr 06 16:00:19 2015 +0200
@@ -125,8 +125,8 @@
           NONE => I
         | SOME id => Protocol_Message.command_positions_yxml id)
         |> error;
-    val {name = (name, _), imports, keywords} = header;
-    val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
+    val {name = (name, _), imports, ...} = header;
+    val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
   in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
 
 fun get_perspective (Node {perspective, ...}) = perspective;