# HG changeset patch
# User wenzelm
# Date 1509565583 -3600
# Node ID df83b66f1d9467da9d4e930430740c97ad858264
# Parent  67595389aa8ab3be61afde72af827ba11dc44655
proper merge (amending fb46c031c841);

diff -r 67595389aa8a -r df83b66f1d94 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)
     }