src/Pure/PIDE/protocol.ML
changeset 59715 4f0d0e4ad68d
parent 59714 ae322325adbb
child 59934 b65c4370f831
--- a/src/Pure/PIDE/protocol.ML	Mon Mar 16 11:30:54 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Mon Mar 16 13:32:31 2015 +0100
@@ -82,7 +82,7 @@
                               (list YXML.string_of_body)))) a;
                         val imports' = map (rpair Position.none) imports;
                         val header = Thy_Header.make (name, Position.none) imports' keywords;
-                      in Document.Deps (master, header, errors) end,
+                      in Document.Deps {master = master, header = header, errors = errors} end,
                     fn (a :: b, c) =>
                       Document.Perspective (bool_atom a, map int_atom b,
                         list (pair int (pair string (list string))) c)]))