proper merge (amending fb46c031c841);
authorwenzelm
Wed, 01 Nov 2017 20:46:23 +0100
changeset 66983 df83b66f1d94
parent 66982 67595389aa8a
child 66984 a1d3e5df0c95
proper merge (amending fb46c031c841);
src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 01 18:37:49 2017 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 01 20:46:23 2017 +0100
@@ -112,7 +112,8 @@
       val keywords1 = keywords ++ other.keywords
       val completion1 = completion ++ other.completion
       val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
-      if ((keywords eq keywords1) && (completion eq completion1)) this
+      if ((keywords eq keywords1) && (completion eq completion1) && (rev_abbrevs eq rev_abbrevs1))
+        this
       else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
     }