--- a/src/Pure/PIDE/resources.ML Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/PIDE/resources.ML Thu Nov 06 11:44:41 2014 +0100
@@ -145,8 +145,8 @@
fun load_thy document last_timing update_time master_dir header text_pos text parents =
let
- val {name = (name, _), ...} = header;
- val _ = Thy_Header.define_keywords header;
+ val (name, _) = #name header;
+ val _ = Thy_Header.define_keywords (#keywords header);
val keywords = Keyword.get_keywords ();
val toks = Outer_Syntax.scan keywords text_pos text;