1.1 --- a/src/Pure/PIDE/document.ML	Wed Feb 27 12:45:19 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Feb 27 16:27:44 2013 +0100
     1.3 @@ -83,7 +83,7 @@
     1.4  fun make_perspective command_ids : perspective =
     1.5    (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
     1.6  
     1.7 -val no_header = ("", Thy_Header.make ("", Position.none) [] [] [], ["Bad theory header"]);
     1.8 +val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
     1.9  val no_perspective = make_perspective [];
    1.10  
    1.11  val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE);
    1.12 @@ -102,9 +102,9 @@
    1.13  
    1.14  fun read_header node span =
    1.15    let
    1.16 -    val (dir, {name = (name, _), imports, keywords, files}) = get_header node;
    1.17 +    val (dir, {name = (name, _), imports, keywords}) = get_header node;
    1.18      val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    1.19 -  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords files) end;
    1.20 +  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
    1.21  
    1.22  fun get_perspective (Node {perspective, ...}) = perspective;
    1.23  fun set_perspective ids =