# HG changeset patch
# User wenzelm
# Date 1507317801 -7200
# Node ID a66f11a0b5b18681e313df9bbc7a3efe41bd2ac5
# Parent  925d10a7a610485f0686b49ec54f93f54787c6c5
even more robust syntax (amending 122df1fde073);

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))