src/Pure/PIDE/resources.ML
changeset 58918 8d36bc5eaed3
parent 58904 f49c4f883c58
child 58923 cb9b69cca999
     1.1 --- a/src/Pure/PIDE/resources.ML	Wed Nov 05 22:39:49 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Thu Nov 06 11:44:41 2014 +0100
     1.3 @@ -145,8 +145,8 @@
     1.4  
     1.5  fun load_thy document last_timing update_time master_dir header text_pos text parents =
     1.6    let
     1.7 -    val {name = (name, _), ...} = header;
     1.8 -    val _ = Thy_Header.define_keywords header;
     1.9 +    val (name, _) = #name header;
    1.10 +    val _ = Thy_Header.define_keywords (#keywords header);
    1.11      val keywords = Keyword.get_keywords ();
    1.12  
    1.13      val toks = Outer_Syntax.scan keywords text_pos text;