src/Pure/PIDE/document.ML

         |> update_node name (edit_node edits)
         |> touch_node name
     | Header header =>
         let
           val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
-          val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
           val header' =
-            (List.app (fn (name, decl) =>
-                Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
+            ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
               handle exn as ERROR _ => Exn.Exn exn;
           val nodes1 = nodes
             |> default_node name
             |> fold default_node imports;
           val nodes2 = nodes1