diff -r 925d10a7a610 -r a66f11a0b5b1 src/Pure/Thy/thy_syntax.scala
--- 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))