src/Pure/Thy/thy_syntax.scala
changeset 48873 18b17f15bc62
parent 48755 393a37003851
child 49414 d7b5fb2e9ca2
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 21 14:54:29 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 21 16:56:18 2012 +0200
@@ -150,7 +150,9 @@
 
     val syntax =
       if (previous.is_init || updated_keywords)
-        (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) }
+        (base_syntax /: nodes.entries) {
+          case (syn, (_, node)) => syn.add_keywords(node.header.keywords)
+        }
       else previous.syntax
 
     val reparse =