src/Pure/PIDE/document.ML
changeset 58918 8d36bc5eaed3
parent 58903 38c72f5f6c2e
child 58923 cb9b69cca999
--- a/src/Pure/PIDE/document.ML	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 06 11:44:41 2014 +0100
@@ -208,7 +208,7 @@
         let
           val imports = map fst (#imports header);
           val errors1 =
-            (Thy_Header.define_keywords header; errors)
+            (Thy_Header.define_keywords (#keywords header); errors)
               handle ERROR msg => errors @ [msg];
           val nodes1 = nodes
             |> default_node name