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