diff -r 4c98d37e1448 -r f164cec7ac22 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Sep 02 10:41:14 2019 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Sep 02 11:46:27 2019 +0200
@@ -82,7 +82,7 @@
           node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
         if (update_header) {
           val node1 = node.update_header(header)
-          if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
+          if (node.header.imports != node1.header.imports ||
               node.header.keywords != node1.header.keywords ||
               node.header.abbrevs != node1.header.abbrevs ||
               node.header.errors != node1.header.errors) syntax_changed0 += name
@@ -102,8 +102,7 @@
           val header = node.header
           val imports_syntax =
             if (header.imports.nonEmpty) {
-              Outer_Syntax.merge(
-                header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
+              Outer_Syntax.merge(header.imports.map(resources.session_base.node_syntax(nodes, _)))
             }
             else resources.session_base.overall_syntax
           Some(imports_syntax + header)