--- a/src/Pure/PIDE/isar_document.ML Sun Sep 18 16:33:30 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Sun Sep 18 19:49:35 2011 +0200
@@ -47,7 +47,8 @@
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
fn ([], a) =>
Document.Header
- (Exn.Res (triple string (list string) (list (pair string bool)) a)),
+ (Exn.Res
+ (triple (pair string string) (list string) (list (pair string bool)) a)),
fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
fn (a, []) => Document.Perspective (map int_atom a)]))
end;