--- a/src/Pure/Thy/thy_syntax.scala Fri Oct 06 21:14:00 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Oct 06 21:23:21 2017 +0200
@@ -101,8 +101,11 @@
else {
val header = node.header
val imports_syntax =
- Outer_Syntax.merge(
- header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
+ if (header.imports.nonEmpty) {
+ Outer_Syntax.merge(
+ header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
+ }
+ else resources.session_base.overall_syntax
Some(imports_syntax + header)
}
nodes += (name -> node.update_syntax(syntax))