src/Pure/PIDE/protocol.ML
changeset 52808 143f225e50f5
parent 52786 9795ea654905
child 52849 199e9fa5a5c2
--- a/src/Pure/PIDE/protocol.ML	Wed Jul 31 10:54:37 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Wed Jul 31 12:14:13 2013 +0200
@@ -56,7 +56,7 @@
                       val imports' = map (rpair Position.none) imports;
                       val header = Thy_Header.make (name, Position.none) imports' keywords;
                     in Document.Deps (master, header, errors) end,
-                  fn (a, []) => Document.Perspective (map int_atom a)]))
+                  fn (a :: b, []) => Document.Perspective (bool_atom a, map int_atom b)]))
             end;
 
         val (removed, assign_update, state') = Document.update old_id new_id edits state;