1.1 --- a/src/Pure/PIDE/document.ML	Tue Feb 26 20:11:11 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Feb 27 12:45:19 2013 +0100
     1.3 @@ -102,9 +102,9 @@
     1.4  
     1.5  fun read_header node span =
     1.6    let
     1.7 -    val (dir, {name = (name, _), imports, keywords, uses}) = get_header node;
     1.8 +    val (dir, {name = (name, _), imports, keywords, files}) = get_header node;
     1.9      val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    1.10 -  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords uses) end;
    1.11 +  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords files) end;
    1.12  
    1.13  fun get_perspective (Node {perspective, ...}) = perspective;
    1.14  fun set_perspective ids =