src/Pure/Thy/thy_syntax.scala
changeset 59086 94b2690ad494
parent 59077 7e0d3da6e6d8
child 59319 677615cba30d
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Dec 03 20:45:20 2014 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Dec 03 22:34:28 2014 +0100
     1.3 @@ -97,8 +97,9 @@
     1.4        val syntax =
     1.5          if (node.is_empty) None
     1.6          else {
     1.7 -          val imports_syntax = node.header.imports.flatMap(a => nodes(a).syntax)
     1.8 -          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(node.header.keywords))
     1.9 +          val header = node.header
    1.10 +          val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
    1.11 +          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
    1.12          }
    1.13        nodes += (name -> node.update_syntax(syntax))
    1.14      }