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 =