src/Pure/Thy/thy_syntax.scala
changeset 66717 67dbf5cdc056
parent 65361 ecefb68dc21d
child 66720 b07192253605
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 17:41:39 2017 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 20:49:42 2017 +0200
     1.3 @@ -101,8 +101,7 @@
     1.4          else {
     1.5            val header = node.header
     1.6            val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
     1.7 -          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
     1.8 -            .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
     1.9 +          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _) + header)
    1.10          }
    1.11        nodes += (name -> node.update_syntax(syntax))
    1.12      }