src/Pure/PIDE/protocol.ML

--- a/src/Pure/PIDE/protocol.ML	Mon Aug 05 15:03:52 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Mon Aug 05 15:29:10 2013 +0200
@@ -58,7 +58,7 @@
                     in Document.Deps (master, header, errors) end,
                   fn (a :: b, c) =>
                     Document.Perspective (bool_atom a, map int_atom b,
-                      list (triple int string (list string)) c)]))
+                      list (pair int (pair string (list string))) c)]))
             end;
 
         val (removed, assign_update, state') = Document.update old_id new_id edits state;