diff -r ae322325adbb -r 4f0d0e4ad68d src/Pure/PIDE/protocol.ML --- 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)]))