--- a/src/Pure/PIDE/protocol.ML Fri Jul 08 22:22:51 2016 +0200
+++ b/src/Pure/PIDE/protocol.ML Sun Jul 10 11:18:35 2016 +0200
@@ -72,7 +72,7 @@
val (master, (name, (imports, (keywords, errors)))) =
pair string (pair string (pair (list string)
(pair (list (pair string
- (option (pair (pair string (list string)) (list string)))))
+ (pair (pair string (list string)) (list string))))
(list YXML.string_of_body)))) a;
val imports' = map (rpair Position.none) imports;
val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;