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