src/Pure/Thy/thy_syntax.scala
changeset 48706 e2b512024eab
parent 47987 4e9df6ffcc6e
child 48707 ba531af91148
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 12:35:24 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 13:21:29 2012 +0200
@@ -153,7 +153,7 @@
 
     val syntax =
       if (previous.is_init || updated_keywords)
-        (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
+        (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) }
       else previous.syntax
 
     val reparse =