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