diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 1cc5b604035..fc8dbea31ce 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -249,7 +249,7 @@ public Attributes CloneAttributes(Attributes attrs) {
         return CloneAttributes(attrs.Prev);
       } else if (attrs is UserSuppliedAttributes) {
         var usa = (UserSuppliedAttributes)attrs;
-        return new UserSuppliedAttributes(Tok(usa.tok), Tok(usa.OpenBrace), Tok(usa.Colon), Tok(usa.CloseBrace), attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
+        return new UserSuppliedAttributes(Tok(usa.tok), Tok(usa.OpenBrace), Tok(usa.CloseBrace), attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
       } else {
         return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev));
       }
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index be2140d660f..dd5f9daf890 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -187,11 +187,6 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, Include include, ModuleD
   theVerifyThisFile = verifyThisFile;
 }
 
-bool IsAttribute() {
-  IToken x = scanner.Peek();
-  return la.kind == _lbrace && x.kind == _colon;
-}
-
 bool IsLabel(bool allowLabel) {
   if (!allowLabel) {
     return false;
@@ -220,18 +215,15 @@ bool IsGets() {
 
 // an existential guard starts with an identifier and is then followed by
 // * a colon (if the first identifier is given an explicit type),
-// * a comma (if there's a list a bound variables and the first one is not given an explicit type),
+// * a comma (if there's a list of bound variables and the first one is not given an explicit type),
 // * a start-attribute (if there's one bound variable and it is not given an explicit type and there are attributes), or
 // * a bored smiley (if there's one bound variable and it is not given an explicit type).
 bool IsExistentialGuard() {
   scanner.ResetPeek();
   if (la.kind == _ident) {
     Token x = scanner.Peek();
-    if (x.kind == _colon || x.kind == _comma || x.kind == _boredSmiley) {
+    if (x.kind == _colon || x.kind == _comma || x.kind == _boredSmiley || x.kind == _lbracecolon) {
       return true;
-    } else if (x.kind == _lbrace) {
-      x = scanner.Peek();
-      return x.kind == _colon;
     }
   }
   return false;
@@ -773,6 +765,7 @@ TOKENS
   ensures = "ensures".
   ghost = "ghost".
   witness = "witness".
+  lbracecolon = "{:".
   lbrace = '{'.
   rbrace = '}'.
   lbracket = '['.
@@ -1593,7 +1586,7 @@ MethodSpec<.List<MaybeFreeExpression> req, List<FrameExpression> mod, List<Maybe
      IToken lbl = null;
   .)
   SYNC
-  ( "modifies" { IF(IsAttribute()) Attribute<ref modAttrs> }
+  ( "modifies" { Attribute<ref modAttrs> }
                FrameExpression<out fe, false, false>         (. Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .)
                { "," FrameExpression<out fe, false, false>   (. Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); .)
                }
@@ -1603,16 +1596,16 @@ MethodSpec<.List<MaybeFreeExpression> req, List<FrameExpression> mod, List<Maybe
                                                              .)
     ]
     ( "requires"
-		  { IF(IsAttribute()) Attribute<ref reqAttrs> }
+		  { Attribute<ref reqAttrs> }
       [ IF(IsLabel(true))
         LabelIdent<out lbl> ":"
       ]
 		  Expression<out e, false, false> OldSemi                (. req.Add(new MaybeFreeExpression(e, isFree, lbl == null ? null : new AssertLabel(lbl, lbl.val), reqAttrs)); .)
     | "ensures"
-      { IF(IsAttribute()) Attribute<ref ensAttrs> }
+      { Attribute<ref ensAttrs> }
       Expression<out e, false, false> OldSemi                (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)
     )
-  | "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, true, false> OldSemi
+  | "decreases" { Attribute<ref decAttrs> } DecreasesList<decreases, true, false> OldSemi
   )
   .
 IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/*!*/ mod, List<Expression/*!*/> decreases,
@@ -1623,12 +1616,12 @@ IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/
      IToken lbl = null;
   .)
   SYNC
-  ( "reads"    { IF(IsAttribute()) Attribute<ref readsAttrs> }
+  ( "reads"    { Attribute<ref readsAttrs> }
                FrameExpression<out fe, false, false>       (. reads.Add(fe); .)
                { "," FrameExpression<out fe, false, false> (. reads.Add(fe); .)
                }
                OldSemi
-  | "modifies" { IF(IsAttribute()) Attribute<ref modAttrs> }
+  | "modifies" { Attribute<ref modAttrs> }
                FrameExpression<out fe, false, false>       (. mod.Add(fe); .)
                { "," FrameExpression<out fe, false, false> (. mod.Add(fe); .)
                }
@@ -1650,7 +1643,7 @@ IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/
                                                                   req.Add(new MaybeFreeExpression(e, isFree, al, null));
                                                                 }
                                                              .)
-    | "ensures" { IF(IsAttribute()) Attribute<ref ensAttrs> }
+    | "ensures" { Attribute<ref ensAttrs> }
       Expression<out e, false, false> OldSemi                (. if (isYield) {
                                                                   yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
                                                                 } else {
@@ -1658,7 +1651,7 @@ IteratorSpec<.List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/
                                                                 }
                                                              .)
     )
-  | "decreases" { IF(IsAttribute()) Attribute<ref decrAttrs> } DecreasesList<decreases, false, false> OldSemi
+  | "decreases" { Attribute<ref decrAttrs> } DecreasesList<decreases, false, false> OldSemi
   )
   .
 Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, List<Formal> formals.>
@@ -2009,7 +2002,7 @@ FunctionSpec<.List<MaybeFreeExpression/*!*/>/*!*/ reqs, List<FrameExpression/*!*
 		 Attributes ensAttrs = null; Attributes reqAttrs = null; .)
   SYNC
   ( "requires"
-	  { IF(IsAttribute()) Attribute<ref reqAttrs> }
+	  { Attribute<ref reqAttrs> }
 		  Expression<out e, false, false> OldSemi                (. reqs.Add(new MaybeFreeExpression(e, false, reqAttrs)); .)
   | "reads"
     PossiblyWildFrameExpression<out fe, false>          (. reads.Add(fe); .)
@@ -2017,7 +2010,7 @@ FunctionSpec<.List<MaybeFreeExpression/*!*/>/*!*/ reqs, List<FrameExpression/*!*
     }
     OldSemi
   | "ensures"
-	  { IF(IsAttribute()) Attribute<ref ensAttrs> }
+	  { Attribute<ref ensAttrs> }
       Expression<out e, false, false> OldSemi                (. ens.Add(new MaybeFreeExpression(e, false, ensAttrs)); .)
   | "decreases"                               (. if (decreases == null) {
                                                    SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
@@ -2503,15 +2496,15 @@ LoopSpec<.List<MaybeFreeExpression> invariants, List<Expression> decreases, ref
     [ "free"                                      (. isFree = true; errors.Deprecated(t, "the 'free' keyword is soon to be deprecated"); .)
     ]
     "invariant"
-    { IF(IsAttribute()) Attribute<ref attrs> }
+    { Attribute<ref attrs> }
     Expression<out e, false, true>                (. invariants.Add(new MaybeFreeExpression(e, isFree, attrs)); .)
     OldSemi
   | SYNC "decreases"
-    { IF(IsAttribute()) Attribute<ref decAttrs> }
+    { Attribute<ref decAttrs> }
     DecreasesList<decreases, true, true>
     OldSemi
   | SYNC "modifies"                               (. mod = mod ?? new List<FrameExpression>(); .)
-    { IF(IsAttribute()) Attribute<ref modAttrs> }
+    { Attribute<ref modAttrs> }
     FrameExpression<out fe, false, true>          (. mod.Add(fe); .)
     { "," FrameExpression<out fe, false, true>    (. mod.Add(fe); .)
     }
@@ -2618,7 +2611,7 @@ AssertStmt<out Statement/*!*/ s, bool inExprContext>
      IToken lbl = null;
   .)
   "assert"                                     (. x = t; .)
-  { IF(IsAttribute()) Attribute<ref attrs> }
+  { Attribute<ref attrs> }
   ( [ IF(IsLabel(!inExprContext))
       LabelIdent<out lbl> ":"
     ]
@@ -2643,7 +2636,7 @@ AssumeStmt<out Statement/*!*/ s>
      IToken dotdotdot = null;
   .)
   "assume"                                     (. x = t; .)
-  { IF(IsAttribute()) Attribute<ref attrs> }
+  { Attribute<ref attrs> }
   ( Expression<out e, false, true>
   | "..."                                      (. dotdotdot = t; .)
   )
@@ -2737,7 +2730,7 @@ ModifyStmt<out Statement s>
      IToken ellipsisToken = null;
   .)
   "modify"           (. tok = t; .)
-  { IF(IsAttribute()) Attribute<ref attrs> }
+  { Attribute<ref attrs> }
   /* Note, there is an ambiguity here, because a curly brace may look like a FrameExpression and
    * may also look like a BlockStmt.  We're happy to parse the former, because if the user intended
    * the latter, then an explicit FrameExpression of {} could be given.
@@ -2771,7 +2764,7 @@ CalcStmt<out Statement s>
      IToken danglingOperator = null;
   .)
   "calc"                                                  (. x = t; .)
-  { IF(IsAttribute()) Attribute<ref attrs> }
+  { Attribute<ref attrs> }
   [ CalcOp<out opTok, out userSuppliedOp>                 (. if (userSuppliedOp.ResultOp(userSuppliedOp) == null) { // guard against non-transitive calcOp (like !=)
                                                                SemErr(opTok, "the main operator of a calculation must be transitive");
                                                              } else {
@@ -3836,7 +3829,7 @@ QuantifierDomain<.out List<BoundVar> bvars, out Attributes attrs, out Expression
   { ","
     IdentTypeOptional<out bv>                  (. bvars.Add(bv); .)
   }
-  { IF(IsAttribute()) Attribute<ref attrs> }
+  { Attribute<ref attrs> }
   [ IF(la.kind == _verticalbar)   /* Coco complains about this ambiguity, thinking that a "|" can follow a body-less forall statement; I don't see how that's possible, but this IF is good and suppresses the reported ambiguity */
     "|"
     Expression<out range, true, true>
@@ -3877,17 +3870,16 @@ Expressions<.List<Expression> args.>
   .
 /*------------------------------------------------------------------------*/
 Attribute<ref Attributes attrs>
-= (. IToken openBrace, colon, closeBrace;
+= (. IToken openBrace, closeBrace;
      IToken x = null;
      var args = new List<Expression>();
   .)
-  "{"                         (. openBrace = t; .)
-  ":"                         (. colon = t; .)
+  "{:"                         (. openBrace = t; .)
   (. ConvertKeywordTokenToIdent(); .)
   NoUSIdent<out x>
   [ Expressions<args> ]
   "}"                         (. closeBrace = t; .)
-  (. attrs = new UserSuppliedAttributes(x, openBrace, colon, closeBrace, args, attrs); .)
+  (. attrs = new UserSuppliedAttributes(x, openBrace, closeBrace, args, attrs); .)
   .
 /*------------------------------------------------------------------------*/
 Ident<out IToken/*!*/ x>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 99a81f6c087..4fed615f885 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -516,19 +516,16 @@ public class UserSuppliedAttributes : Attributes
   {
     public readonly IToken tok;  // may be null, if the attribute was constructed internally
     public readonly IToken OpenBrace;
-    public readonly IToken Colon;
     public readonly IToken CloseBrace;
     public bool Recognized;  // set to true to indicate an attribute that is processed by some part of Dafny; this allows it to be colored in the IDE
-    public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken colon, IToken closeBrace, List<Expression> args, Attributes prev)
+    public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, List<Expression> args, Attributes prev)
       : base(tok.val, args, prev) {
       Contract.Requires(tok != null);
       Contract.Requires(openBrace != null);
-      Contract.Requires(colon != null);
       Contract.Requires(closeBrace != null);
       Contract.Requires(args != null);
       this.tok = tok;
       OpenBrace = openBrace;
-      Colon = colon;
       CloseBrace = closeBrace;
     }
   }
@@ -6210,9 +6207,8 @@ public override IEnumerable<Statement> SubStatements {
     public void AddCustomizedErrorMessage(IToken tok, string s) {
       var args = new List<Expression>() { new StringLiteralExpr(tok, s, true) };
       IToken openBrace = tok;
-      IToken colon = new Token(tok.line, tok.col + 1);
       IToken closeBrace = new Token(tok.line, tok.col + 7 + s.Length + 1); // where 7 = length(":error ")
-      this.Attributes = new UserSuppliedAttributes(tok, openBrace, colon, closeBrace, args, this.Attributes);
+      this.Attributes = new UserSuppliedAttributes(tok, openBrace, closeBrace, args, this.Attributes);
     }
   }
 
@@ -10719,9 +10715,8 @@ public MaybeFreeExpression(Expression e, bool isFree, AssertLabel/*?*/ label, At
     public void AddCustomizedErrorMessage(IToken tok, string s) {
       var args = new List<Expression>() { new StringLiteralExpr(tok, s, true) };
       IToken openBrace = tok;
-      IToken colon = new Token(tok.line, tok.col + 1);
       IToken closeBrace = new Token(tok.line, tok.col + 7 + s.Length + 1); // where 7 = length(":error ")
-      this.Attributes = new UserSuppliedAttributes(tok, openBrace, colon, closeBrace, args, this.Attributes);
+      this.Attributes = new UserSuppliedAttributes(tok, openBrace, closeBrace, args, this.Attributes);
     }
   }
 
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index f282832cc9f..c018d81c233 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -93,22 +93,23 @@ public class Parser {
 	public const int _ensures = 71;
 	public const int _ghost = 72;
 	public const int _witness = 73;
-	public const int _lbrace = 74;
-	public const int _rbrace = 75;
-	public const int _lbracket = 76;
-	public const int _rbracket = 77;
-	public const int _openparen = 78;
-	public const int _closeparen = 79;
-	public const int _openAngleBracket = 80;
-	public const int _closeAngleBracket = 81;
-	public const int _eq = 82;
-	public const int _neq = 83;
-	public const int _neqAlt = 84;
-	public const int _star = 85;
-	public const int _notIn = 86;
-	public const int _ellipsis = 87;
-	public const int _reveal = 88;
-	public const int maxT = 155;
+	public const int _lbracecolon = 74;
+	public const int _lbrace = 75;
+	public const int _rbrace = 76;
+	public const int _lbracket = 77;
+	public const int _rbracket = 78;
+	public const int _openparen = 79;
+	public const int _closeparen = 80;
+	public const int _openAngleBracket = 81;
+	public const int _closeAngleBracket = 82;
+	public const int _eq = 83;
+	public const int _neq = 84;
+	public const int _neqAlt = 85;
+	public const int _star = 86;
+	public const int _notIn = 87;
+	public const int _ellipsis = 88;
+	public const int _reveal = 89;
+	public const int maxT = 156;
 
   const bool _T = true;
   const bool _x = false;
@@ -294,11 +295,6 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, Include include, ModuleD
   theVerifyThisFile = verifyThisFile;
 }
 
-bool IsAttribute() {
-  IToken x = scanner.Peek();
-  return la.kind == _lbrace && x.kind == _colon;
-}
-
 bool IsLabel(bool allowLabel) {
   if (!allowLabel) {
     return false;
@@ -327,18 +323,15 @@ bool IsGets() {
 
 // an existential guard starts with an identifier and is then followed by
 // * a colon (if the first identifier is given an explicit type),
-// * a comma (if there's a list a bound variables and the first one is not given an explicit type),
+// * a comma (if there's a list of bound variables and the first one is not given an explicit type),
 // * a start-attribute (if there's one bound variable and it is not given an explicit type and there are attributes), or
 // * a bored smiley (if there's one bound variable and it is not given an explicit type).
 bool IsExistentialGuard() {
   scanner.ResetPeek();
   if (la.kind == _ident) {
     Token x = scanner.Peek();
-    if (x.kind == _colon || x.kind == _comma || x.kind == _boredSmiley) {
+    if (x.kind == _colon || x.kind == _comma || x.kind == _boredSmiley || x.kind == _lbracecolon) {
       return true;
-    } else if (x.kind == _lbrace) {
-      x = scanner.Peek();
-      return x.kind == _colon;
     }
   }
   return false;
@@ -825,7 +818,7 @@ void Dafny() {
 		// theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
 		Contract.Assert(defaultModule != null);
 		
-		while (la.kind == 89) {
+		while (la.kind == 90) {
 			Get();
 			Expect(24);
 			{
@@ -870,7 +863,7 @@ void TopDecl(ModuleDefinition module, List<MemberDecl/*!*/> membersDefaultClass,
 			DeclModifier(ref dmod);
 		}
 		switch (la.kind) {
-		case 54: case 55: case 91: {
+		case 54: case 55: case 92: {
 			SubModuleDecl(dmod, module, out submodule);
 			var litmod = submodule as LiteralModuleDecl;
 			if (litmod != null && litmod.ModuleDef.PrefixIds.Count != 0) {
@@ -911,17 +904,17 @@ void TopDecl(ModuleDefinition module, List<MemberDecl/*!*/> membersDefaultClass,
 			module.TopLevelDecls.Add(trait); 
 			break;
 		}
-		case 46: case 47: case 48: case 49: case 50: case 51: case 60: case 61: case 65: case 66: case 67: case 104: {
+		case 46: case 47: case 48: case 49: case 50: case 51: case 60: case 61: case 65: case 66: case 67: case 105: {
 			ClassMemberDecl(dmod, membersDefaultClass, false, true, !DafnyOptions.O.AllowGlobals,
 !isTopLevel && DafnyOptions.O.IronDafny && isAbstract);
 			break;
 		}
-		default: SynErr(156); break;
+		default: SynErr(157); break;
 		}
 	}
 
 	void DeclModifier(ref DeclModifierData dmod) {
-		if (la.kind == 90) {
+		if (la.kind == 91) {
 			Get();
 			dmod.IsAbstract = true;  CheckAndSetToken(ref dmod.AbstractToken); 
 		} else if (la.kind == 72) {
@@ -933,7 +926,7 @@ void DeclModifier(ref DeclModifierData dmod) {
 		} else if (la.kind == 53) {
 			Get();
 			dmod.IsProtected = true; CheckAndSetToken(ref dmod.ProtectedToken); 
-		} else SynErr(157);
+		} else SynErr(158);
 	}
 
 	void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDecl submodule) {
@@ -948,7 +941,7 @@ void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDec
 		bool opened = false;
 		CheckDeclModifiers(dmod, "Modules", AllowedDeclModifiers.Abstract | AllowedDeclModifiers.Protected);
 		
-		if (la.kind == 91) {
+		if (la.kind == 92) {
 			Get();
 			while (la.kind == 74) {
 				Attribute(ref attrs);
@@ -959,23 +952,23 @@ void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDec
 				Get();
 				NoUSIdent(out id);
 			}
-			if (la.kind == 92) {
+			if (la.kind == 93) {
 				Get();
 				ModuleName(out idRefined);
 			}
 			module = new ModuleDefinition(id, id.val, prefixIds, isAbstract, isProtected, false, idRefined, parent, attrs, false); module.IsToBeVerified = theVerifyThisFile; 
-			Expect(74);
+			Expect(75);
 			module.BodyStartTok = t; 
 			while (StartOf(1)) {
 				TopDecl(module, namedModuleDefaultClassMembers, /* isTopLevel */ false, isAbstract);
 			}
-			Expect(75);
+			Expect(76);
 			module.BodyEndTok = t;
 			module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
 			submodule = new LiteralModuleDecl(module, parent); 
 		} else if (la.kind == 54) {
 			Get();
-			if (la.kind == 93) {
+			if (la.kind == 94) {
 				Get();
 				opened = true;
 			}
@@ -990,7 +983,7 @@ void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDec
 				idPath.Insert(0, id);
 				submodule = new AliasModuleDecl(idPath, id, parent, opened, idExports);
 				
-			} else if (la.kind == 94) {
+			} else if (la.kind == 95) {
 				Get();
 				QualifiedModuleExport(out idPath, out idExports);
 				submodule = new AliasModuleDecl(idPath, id, parent, opened, idExports); 
@@ -998,9 +991,9 @@ void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDec
 				Get();
 				QualifiedModuleExport(out idPath, out idExports);
 				submodule = new ModuleFacadeDecl(idPath, id, parent, opened, idExports); 
-			} else SynErr(158);
+			} else SynErr(159);
 			if (la.kind == 34) {
-				while (!(la.kind == 0 || la.kind == 34)) {SynErr(159); Get();}
+				while (!(la.kind == 0 || la.kind == 34)) {SynErr(160); Get();}
 				Get();
 				errors.Deprecated(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); 
 			}
@@ -1018,8 +1011,8 @@ void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDec
 			if (la.kind == 1 || la.kind == 2) {
 				ExportIdent(out exportId);
 			}
-			while (la.kind == 95 || la.kind == 96 || la.kind == 97) {
-				if (la.kind == 95) {
+			while (la.kind == 96 || la.kind == 97 || la.kind == 98) {
+				if (la.kind == 96) {
 					Get();
 					if (la.kind == 1 || la.kind == 2) {
 						ModuleExportSignature(true, out exsig);
@@ -1029,11 +1022,11 @@ void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDec
 							ModuleExportSignature(true, out exsig);
 							exports.Add(exsig); 
 						}
-					} else if (la.kind == 85) {
+					} else if (la.kind == 86) {
 						Get();
 						provideAll = true; 
-					} else SynErr(160);
-				} else if (la.kind == 96) {
+					} else SynErr(161);
+				} else if (la.kind == 97) {
 					Get();
 					if (la.kind == 1 || la.kind == 2) {
 						ModuleExportSignature(false, out exsig);
@@ -1043,10 +1036,10 @@ void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDec
 							ModuleExportSignature(false, out exsig);
 							exports.Add(exsig); 
 						}
-					} else if (la.kind == 85) {
+					} else if (la.kind == 86) {
 						Get();
 						revealAll = true; 
-					} else SynErr(161);
+					} else SynErr(162);
 				} else {
 					Get();
 					ExportIdent(out id);
@@ -1063,7 +1056,7 @@ void SubModuleDecl(DeclModifierData dmod, ModuleDefinition parent, out ModuleDec
 			}
 			submodule = new ModuleExportDecl(exportId, parent, exports, extends, provideAll, revealAll, isDefault);
 			
-		} else SynErr(162);
+		} else SynErr(163);
 	}
 
 	void ClassDecl(DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) {
@@ -1079,16 +1072,16 @@ void ClassDecl(DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out Cla
 		CheckDeclModifiers(dmodClass, "Classes", AllowedDeclModifiers.None);
 		DeclModifierData dmod;
 		
-		while (!(la.kind == 0 || la.kind == 56)) {SynErr(163); Get();}
+		while (!(la.kind == 0 || la.kind == 56)) {SynErr(164); Get();}
 		Expect(56);
 		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		NoUSIdent(out id);
-		if (la.kind == 80) {
+		if (la.kind == 81) {
 			GenericParameters(typeArgs, true);
 		}
-		if (la.kind == 97) {
+		if (la.kind == 98) {
 			Get();
 			Type(out trait);
 			traits.Add(trait); 
@@ -1098,7 +1091,7 @@ void ClassDecl(DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out Cla
 				traits.Add(trait); 
 			}
 		}
-		Expect(74);
+		Expect(75);
 		bodyStart = t;  
 		while (StartOf(4)) {
 			dmod = new DeclModifierData(); 
@@ -1107,7 +1100,7 @@ void ClassDecl(DeclModifierData dmodClass, ModuleDefinition/*!*/ module, out Cla
 			}
 			ClassMemberDecl(dmod, members, true, false, false, false);
 		}
-		Expect(75);
+		Expect(76);
 		c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits);
 		c.BodyStartTok = bodyStart;
 		c.BodyEndTok = t;
@@ -1126,21 +1119,21 @@ void DatatypeDecl(DeclModifierData dmod, ModuleDefinition/*!*/ module, out Datat
 		CheckDeclModifiers(dmod, "Datatypes or codatatypes", AllowedDeclModifiers.None);
 		var members = new List<MemberDecl>();
 		
-		while (!(la.kind == 0 || la.kind == 58 || la.kind == 59)) {SynErr(164); Get();}
+		while (!(la.kind == 0 || la.kind == 58 || la.kind == 59)) {SynErr(165); Get();}
 		if (la.kind == 58) {
 			Get();
 		} else if (la.kind == 59) {
 			Get();
 			co = true; 
-		} else SynErr(165);
+		} else SynErr(166);
 		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		NoUSIdent(out id);
-		if (la.kind == 80) {
+		if (la.kind == 81) {
 			GenericParameters(typeArgs, true);
 		}
-		Expect(94);
+		Expect(95);
 		bodyStart = t; 
 		if (la.kind == 27) {
 			Get();
@@ -1150,7 +1143,7 @@ void DatatypeDecl(DeclModifierData dmod, ModuleDefinition/*!*/ module, out Datat
 			Get();
 			DatatypeMemberDecl(ctors);
 		}
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			TypeMembers(module, members);
 		}
 		if (co) {
@@ -1179,7 +1172,7 @@ void NewtypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDec
 			Attribute(ref attrs);
 		}
 		NoUSIdent(out id);
-		Expect(94);
+		Expect(95);
 		if (IsIdentColonOrBar()) {
 			NoUSIdent(out bvId);
 			if (la.kind == 25) {
@@ -1197,7 +1190,7 @@ void NewtypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDec
 				Expect(73);
 				Expression(out witness, false, true);
 			}
-			if (la.kind == 74) {
+			if (la.kind == 75) {
 				TypeMembers(module, members);
 			}
 			var witnessKind = witness == null ? SubsetTypeDecl.WKind.None :
@@ -1205,11 +1198,11 @@ void NewtypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDec
 			td = new NewtypeDecl(id, id.val, module, new BoundVar(bvId, bvId.val, baseType), constraint, witnessKind, witness, members, attrs); 
 		} else if (StartOf(5)) {
 			Type(out baseType);
-			if (la.kind == 74) {
+			if (la.kind == 75) {
 				TypeMembers(module, members);
 			}
 			td = new NewtypeDecl(id, id.val, module, baseType, members, attrs); 
-		} else SynErr(166);
+		} else SynErr(167);
 	}
 
 	void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelDecl td) {
@@ -1229,13 +1222,13 @@ void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelD
 			Attribute(ref attrs);
 		}
 		NoUSIdent(out id);
-		while (la.kind == 78) {
+		while (la.kind == 79) {
 			TypeParameterCharacteristics(ref characteristics);
 		}
-		if (la.kind == 80) {
+		if (la.kind == 81) {
 			GenericParameters(typeArgs, true);
 		}
-		if (la.kind == 94) {
+		if (la.kind == 95) {
 			Get();
 			if (IsIdentColonOrBar()) {
 				NoUSIdent(out bvId);
@@ -1264,7 +1257,7 @@ void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelD
 				td = new TypeSynonymDecl(id, id.val, characteristics, typeArgs, module, ty, attrs);
 				kind = "Type synonym";
 				
-			} else SynErr(167);
+			} else SynErr(168);
 		}
 		if (td == null) {
 		 if (module is DefaultModuleDecl) {
@@ -1276,7 +1269,7 @@ void OtherTypeDecl(DeclModifierData dmod, ModuleDefinition module, out TopLevelD
 		
 		CheckDeclModifiers(dmod, kind, AllowedDeclModifiers.None); 
 		if (la.kind == 34) {
-			while (!(la.kind == 0 || la.kind == 34)) {SynErr(168); Get();}
+			while (!(la.kind == 0 || la.kind == 34)) {SynErr(169); Get();}
 			Get();
 			errors.Deprecated(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); 
 		}
@@ -1306,19 +1299,19 @@ void IteratorDecl(DeclModifierData dmod, ModuleDefinition module, out IteratorDe
 		IToken bodyEnd = Token.NoToken;
 		CheckDeclModifiers(dmod, "Iterators", AllowedDeclModifiers.None);
 		
-		while (!(la.kind == 0 || la.kind == 64)) {SynErr(169); Get();}
+		while (!(la.kind == 0 || la.kind == 64)) {SynErr(170); Get();}
 		Expect(64);
 		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		NoUSIdent(out id);
-		if (la.kind == 78 || la.kind == 80) {
-			if (la.kind == 80) {
+		if (la.kind == 79 || la.kind == 81) {
+			if (la.kind == 81) {
 				GenericParameters(typeArgs, true);
 			}
 			Formals(true, true, false, ins);
-			if (la.kind == 99 || la.kind == 100) {
-				if (la.kind == 99) {
+			if (la.kind == 100 || la.kind == 101) {
+				if (la.kind == 100) {
 					Get();
 				} else {
 					Get();
@@ -1326,14 +1319,14 @@ void IteratorDecl(DeclModifierData dmod, ModuleDefinition module, out IteratorDe
 				}
 				Formals(false, true, false, outs);
 			}
-		} else if (la.kind == 87) {
+		} else if (la.kind == 88) {
 			Get();
 			signatureEllipsis = t; 
-		} else SynErr(170);
+		} else SynErr(171);
 		while (StartOf(6)) {
 			IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);
 		}
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			BlockStmt(out body, out bodyStart, out bodyEnd);
 		}
 		iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
@@ -1358,16 +1351,16 @@ void TraitDecl(DeclModifierData dmodIn, ModuleDefinition/*!*/ module, out TraitD
 		IToken bodyStart;
 		DeclModifierData dmod;
 		
-		while (!(la.kind == 0 || la.kind == 57)) {SynErr(171); Get();}
+		while (!(la.kind == 0 || la.kind == 57)) {SynErr(172); Get();}
 		Expect(57);
 		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		NoUSIdent(out id);
-		if (la.kind == 80) {
+		if (la.kind == 81) {
 			GenericParameters(typeArgs, true);
 		}
-		Expect(74);
+		Expect(75);
 		bodyStart = t; 
 		while (StartOf(4)) {
 			dmod  = new DeclModifierData(); 
@@ -1376,7 +1369,7 @@ void TraitDecl(DeclModifierData dmodIn, ModuleDefinition/*!*/ module, out TraitD
 			}
 			ClassMemberDecl(dmod, members, true, false, false, false);
 		}
-		Expect(75);
+		Expect(76);
 		trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
 		trait.BodyStartTok = bodyStart;
 		trait.BodyEndTok = t;
@@ -1413,26 +1406,24 @@ void ClassMemberDecl(DeclModifierData dmod, List<MemberDecl> mm, bool allowConst
 			
 			MethodDecl(dmod, allowConstructors, isWithinAbstractModule, out m);
 			mm.Add(m); 
-		} else SynErr(172);
+		} else SynErr(173);
 	}
 
 	void Attribute(ref Attributes attrs) {
-		IToken openBrace, colon, closeBrace;
+		IToken openBrace, closeBrace;
 		IToken x = null;
 		var args = new List<Expression>();
 		
 		Expect(74);
 		openBrace = t; 
-		Expect(25);
-		colon = t; 
 		ConvertKeywordTokenToIdent(); 
 		NoUSIdent(out x);
 		if (StartOf(8)) {
 			Expressions(args);
 		}
-		Expect(75);
+		Expect(76);
 		closeBrace = t; 
-		attrs = new UserSuppliedAttributes(x, openBrace, colon, closeBrace, args, attrs); 
+		attrs = new UserSuppliedAttributes(x, openBrace, closeBrace, args, attrs); 
 	}
 
 	void NoUSIdent(out IToken/*!*/ x) {
@@ -1465,7 +1456,7 @@ void QualifiedModuleExportSuffix(List<IToken> ids, List<IToken> exports) {
 			if (la.kind == 1 || la.kind == 2) {
 				ExportIdent(out id);
 				exports.Add(id); 
-			} else if (la.kind == 74) {
+			} else if (la.kind == 75) {
 				Get();
 				ExportIdent(out id);
 				exports.Add(id); 
@@ -1474,9 +1465,9 @@ void QualifiedModuleExportSuffix(List<IToken> ids, List<IToken> exports) {
 					ExportIdent(out id);
 					exports.Add(id); 
 				}
-				Expect(75);
-			} else SynErr(173);
-		} else SynErr(174);
+				Expect(76);
+			} else SynErr(174);
+		} else SynErr(175);
 	}
 
 	void QualifiedModuleExport(out List<IToken> ids, out List<IToken> exports) {
@@ -1518,7 +1509,7 @@ void TypeNameOrCtorSuffix(out IToken id) {
 		} else if (la.kind == 2) {
 			Get();
 			id = t; 
-		} else SynErr(175);
+		} else SynErr(176);
 	}
 
 	void Ident(out IToken/*!*/ x) {
@@ -1534,13 +1525,13 @@ void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs, bool allowVarianc
 		TypeParameter.TPVarianceSyntax variance = TypeParameter.TPVarianceSyntax.NonVariant_Strict;  // assignment is to please compiler
 		characteristics = new TypeParameter.TypeParameterCharacteristics(false);
 		
-		Expect(80);
+		Expect(81);
 		if (StartOf(9)) {
 			Variance(out variance);
 			if (!allowVariance) { SemErr(t, "type-parameter variance is not allowed to be specified in this context"); } 
 		}
 		NoUSIdent(out id);
-		while (la.kind == 78) {
+		while (la.kind == 79) {
 			TypeParameterCharacteristics(ref characteristics);
 		}
 		typeArgs.Add(new TypeParameter(id, id.val, variance, characteristics)); 
@@ -1554,12 +1545,12 @@ void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs, bool allowVarianc
 				if (!allowVariance) { SemErr(t, "type-parameter variance is not allowed to be specified in this context"); } 
 			}
 			NoUSIdent(out id);
-			while (la.kind == 78) {
+			while (la.kind == 79) {
 				TypeParameterCharacteristics(ref characteristics);
 			}
 			typeArgs.Add(new TypeParameter(id, id.val, variance, characteristics)); 
 		}
-		Expect(81);
+		Expect(82);
 	}
 
 	void Type(out Type ty) {
@@ -1577,7 +1568,7 @@ void FieldDecl(DeclModifierData dmod, bool isValueType, List<MemberDecl> mm) {
 		 mm = new List<MemberDecl>();
 		}
 		
-		while (!(la.kind == 0 || la.kind == 60)) {SynErr(176); Get();}
+		while (!(la.kind == 0 || la.kind == 60)) {SynErr(177); Get();}
 		Expect(60);
 		if (isValueType) {
 		 SemErr(t, "mutable fields are now allowed in value types");
@@ -1607,7 +1598,7 @@ void ConstantFieldDecl(DeclModifierData dmod, List<MemberDecl/*!*/>/*!*/ mm, boo
 		}
 		CheckDeclModifiers(dmod, "Fields", AllowedDeclModifiers.Ghost | AllowedDeclModifiers.Static);
 		
-		while (!(la.kind == 0 || la.kind == 61)) {SynErr(177); Get();}
+		while (!(la.kind == 0 || la.kind == 61)) {SynErr(178); Get();}
 		Expect(61);
 		while (la.kind == 74) {
 			Attribute(ref attrs);
@@ -1672,14 +1663,14 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
 				Attribute(ref attrs);
 			}
 			FuMe_Ident(out id);
-			if (la.kind == 78 || la.kind == 80) {
-				if (la.kind == 80) {
+			if (la.kind == 79 || la.kind == 81) {
+				if (la.kind == 81) {
 					GenericParameters(typeArgs, false);
 				}
 				Formals(true, isFunctionMethod, isTwoState, formals);
 				Expect(25);
 				if (FollowedByColon()) {
-					Expect(78);
+					Expect(79);
 					IToken resultId;
 					Type ty;
 					bool isGhost;
@@ -1689,14 +1680,14 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
 					Contract.Assert(!isGhost && !isOld);
 					result = new Formal(resultId, resultId.val, ty, false, false, false);
 					
-					Expect(79);
+					Expect(80);
 				} else if (StartOf(5)) {
 					Type(out returnType);
-				} else SynErr(178);
-			} else if (la.kind == 87) {
+				} else SynErr(179);
+			} else if (la.kind == 88) {
 				Get();
 				signatureEllipsis = t; 
-			} else SynErr(179);
+			} else SynErr(180);
 		} else if (la.kind == 47) {
 			Get();
 			isPredicate = true; 
@@ -1719,11 +1710,11 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
 			}
 			NoUSIdent(out id);
 			if (StartOf(10)) {
-				if (la.kind == 80) {
+				if (la.kind == 81) {
 					GenericParameters(typeArgs, false);
 				}
 				missingOpenParen = true; 
-				if (la.kind == 78) {
+				if (la.kind == 79) {
 					Formals(true, isFunctionMethod, isTwoState, formals);
 					missingOpenParen = false; 
 				}
@@ -1732,10 +1723,10 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
 					Get();
 					SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); 
 				}
-			} else if (la.kind == 87) {
+			} else if (la.kind == 88) {
 				Get();
 				signatureEllipsis = t; 
-			} else SynErr(180);
+			} else SynErr(181);
 		} else if (la.kind == 48) {
 			Contract.Assert(!isTwoState);  // the IsFunctionDecl check checks that "twostate" is not followed by "inductive"
 			
@@ -1749,11 +1740,11 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
 				Attribute(ref attrs);
 			}
 			FuMe_Ident(out id);
-			if (la.kind == 76 || la.kind == 78 || la.kind == 80) {
-				if (la.kind == 80) {
+			if (la.kind == 77 || la.kind == 79 || la.kind == 81) {
+				if (la.kind == 81) {
 					GenericParameters(typeArgs, false);
 				}
-				if (la.kind == 76) {
+				if (la.kind == 77) {
 					KType(ref kType);
 				}
 				Formals(true, isFunctionMethod, false, formals);
@@ -1761,10 +1752,10 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
 					Get();
 					SemErr(t, "inductive predicates do not have an explicitly declared return type; it is always bool"); 
 				}
-			} else if (la.kind == 87) {
+			} else if (la.kind == 88) {
 				Get();
 				signatureEllipsis = t; 
-			} else SynErr(181);
+			} else SynErr(182);
 		} else if (la.kind == 50) {
 			Contract.Assert(!isTwoState);  // the IsFunctionDecl check checks that "twostate" is not followed by "copredicate"
 			
@@ -1777,11 +1768,11 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
 				Attribute(ref attrs);
 			}
 			NoUSIdent(out id);
-			if (la.kind == 76 || la.kind == 78 || la.kind == 80) {
-				if (la.kind == 80) {
+			if (la.kind == 77 || la.kind == 79 || la.kind == 81) {
+				if (la.kind == 81) {
 					GenericParameters(typeArgs, false);
 				}
-				if (la.kind == 76) {
+				if (la.kind == 77) {
 					KType(ref kType);
 				}
 				Formals(true, isFunctionMethod, false, formals);
@@ -1789,16 +1780,16 @@ void FunctionDecl(DeclModifierData dmod, bool isWithinAbstractModule, out Functi
 					Get();
 					SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); 
 				}
-			} else if (la.kind == 87) {
+			} else if (la.kind == 88) {
 				Get();
 				signatureEllipsis = t; 
-			} else SynErr(182);
-		} else SynErr(183);
+			} else SynErr(183);
+		} else SynErr(184);
 		decreases = isIndPredicate || isCoPredicate ? null : new List<Expression/*!*/>(); 
 		while (StartOf(11)) {
 			FunctionSpec(reqs, reads, ens, decreases);
 		}
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			FunctionBody(out body, out bodyStart, out bodyEnd);
 		}
 		if (!isWithinAbstractModule && DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 &&
@@ -1863,7 +1854,7 @@ void MethodDecl(DeclModifierData dmod, bool allowConstructor, bool isWithinAbstr
 		string caption = "";
 		FixpointPredicate.KType kType = FixpointPredicate.KType.Unspecified;
 		
-		while (!(StartOf(12))) {SynErr(184); Get();}
+		while (!(StartOf(12))) {SynErr(185); Get();}
 		switch (la.kind) {
 		case 65: {
 			Get();
@@ -1885,7 +1876,7 @@ void MethodDecl(DeclModifierData dmod, bool allowConstructor, bool isWithinAbstr
 			 | AllowedDeclModifiers.Protected; 
 			break;
 		}
-		case 104: {
+		case 105: {
 			Get();
 			isCoLemma = true; caption = "Comethods";
 			allowed = AllowedDeclModifiers.AlreadyGhost | AllowedDeclModifiers.Static
@@ -1921,7 +1912,7 @@ void MethodDecl(DeclModifierData dmod, bool allowConstructor, bool isWithinAbstr
 			
 			break;
 		}
-		default: SynErr(185); break;
+		default: SynErr(186); break;
 		}
 		keywordToken = t;
 		CheckDeclModifiers(dmod, caption, allowed); 
@@ -1939,29 +1930,29 @@ void MethodDecl(DeclModifierData dmod, bool allowConstructor, bool isWithinAbstr
 		 }
 		}
 		
-		if (la.kind == 76 || la.kind == 78 || la.kind == 80) {
-			if (la.kind == 80) {
+		if (la.kind == 77 || la.kind == 79 || la.kind == 81) {
+			if (la.kind == 81) {
 				GenericParameters(typeArgs, false);
 			}
-			if (la.kind == 76) {
+			if (la.kind == 77) {
 				KType(ref kType);
 				if (!(isCoLemma || isIndLemma)) { SemErr(t, "type of _k can only be specified for inductive lemmas and co-lemmas"); } 
 			}
 			var isCompilable = (isPlainOlMethod && !dmod.IsGhost) || isConstructor; 
 			Formals(true, isCompilable, isTwoStateLemma, ins);
-			if (la.kind == 100) {
+			if (la.kind == 101) {
 				Get();
 				if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 
 				Formals(false, isCompilable, false, outs);
 			}
-		} else if (la.kind == 87) {
+		} else if (la.kind == 88) {
 			Get();
 			signatureEllipsis = t; 
-		} else SynErr(186);
+		} else SynErr(187);
 		while (StartOf(13)) {
 			MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs, caption, isConstructor);
 		}
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			if (isConstructor) {
 				DividedBlockStmt dividedBody; 
 				DividedBlockStmt(out dividedBody, out bodyStart, out bodyEnd);
@@ -2010,7 +2001,7 @@ void DatatypeMemberDecl(List<DatatypeCtor/*!*/>/*!*/ ctors) {
 			Attribute(ref attrs);
 		}
 		NoUSIdent(out id);
-		if (la.kind == 78) {
+		if (la.kind == 79) {
 			FormalsOptionalIds(formals);
 		}
 		ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); 
@@ -2019,7 +2010,7 @@ void DatatypeMemberDecl(List<DatatypeCtor/*!*/>/*!*/ ctors) {
 	void TypeMembers(ModuleDefinition/*!*/ module, List<MemberDecl> members ) {
 		DeclModifierData dmod;
 		
-		Expect(74);
+		Expect(75);
 		while (StartOf(4)) {
 			dmod = new DeclModifierData(); 
 			while (StartOf(2)) {
@@ -2027,12 +2018,12 @@ void TypeMembers(ModuleDefinition/*!*/ module, List<MemberDecl> members ) {
 			}
 			ClassMemberDecl(dmod, members, false, true, false, module.IsAbstract);
 		}
-		Expect(75);
+		Expect(76);
 	}
 
 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; 
-		Expect(78);
+		Expect(79);
 		if (StartOf(14)) {
 			TypeIdentOptional(out id, out name, out ty, out isGhost);
 			formals.Add(new Formal(id, name, ty, true, isGhost)); 
@@ -2042,7 +2033,7 @@ void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
 				formals.Add(new Formal(id, name, ty, true, isGhost)); 
 			}
 		}
-		Expect(79);
+		Expect(80);
 	}
 
 	void FIdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
@@ -2054,14 +2045,14 @@ void FIdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
 		} else if (la.kind == 2) {
 			Get();
 			id = t; 
-		} else SynErr(187);
+		} else SynErr(188);
 		Expect(25);
 		Type(out ty);
 	}
 
 	void OldSemi() {
 		if (la.kind == 34) {
-			while (!(la.kind == 0 || la.kind == 34)) {SynErr(188); Get();}
+			while (!(la.kind == 0 || la.kind == 34)) {SynErr(189); Get();}
 			Get();
 			errors.DeprecatedStyle(t, "deprecated style: a semi-colon is not needed here"); 
 		}
@@ -2077,7 +2068,7 @@ void CIdentType(out IToken/*!*/ id, out Type ty) {
 		} else if (la.kind == 2) {
 			Get();
 			id = t; 
-		} else SynErr(189);
+		} else SynErr(190);
 		if (la.kind == 25) {
 			Get();
 			Type(out ty);
@@ -2099,20 +2090,20 @@ void Expression(out Expression e, bool allowSemi, bool allowLambda, bool allowBi
 	}
 
 	void TypeParameterCharacteristics(ref TypeParameter.TypeParameterCharacteristics characteristics) {
-		Expect(78);
+		Expect(79);
 		TPCharOption(ref characteristics);
 		while (la.kind == 26) {
 			Get();
 			TPCharOption(ref characteristics);
 		}
-		Expect(79);
+		Expect(80);
 	}
 
 	void GIdentType(bool allowGhostKeyword, bool allowNewKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost, out bool isOld) {
 		Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
 		Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
 		isGhost = false; isOld = allowNewKeyword; 
-		while (la.kind == 72 || la.kind == 98) {
+		while (la.kind == 72 || la.kind == 99) {
 			if (la.kind == 72) {
 				Get();
 				if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } 
@@ -2191,7 +2182,7 @@ void TypeIdentOptional(out IToken/*!*/ id, out string/*!*/ identName, out Type/*
 			id = t; name = id.val;
 			Expect(25);
 			Type(out ty);
-		} else SynErr(190);
+		} else SynErr(191);
 		if (name != null) {
 		 identName = name;
 		} else {
@@ -2354,7 +2345,7 @@ void TypeAndToken(out IToken tok, out Type ty, bool inExpressionContext) {
 			
 			break;
 		}
-		case 78: {
+		case 79: {
 			Get();
 			tok = t; tupleArgTypes = new List<Type>(); 
 			if (StartOf(5)) {
@@ -2366,7 +2357,7 @@ void TypeAndToken(out IToken tok, out Type ty, bool inExpressionContext) {
 					tupleArgTypes.Add(ty); 
 				}
 			}
-			Expect(79);
+			Expect(80);
 			if (tupleArgTypes.Count == 1) {
 			 // just return the type 'ty'
 			} else {
@@ -2391,16 +2382,16 @@ void TypeAndToken(out IToken tok, out Type ty, bool inExpressionContext) {
 			ty = new UserDefinedType(e.tok, e); 
 			break;
 		}
-		default: SynErr(191); break;
+		default: SynErr(192); break;
 		}
-		if (la.kind == 107 || la.kind == 108 || la.kind == 109) {
+		if (la.kind == 108 || la.kind == 109 || la.kind == 110) {
 			int arrowKind = 0; /* 0: any, 1: partial, 2: total */
 			Type t2;
 			
-			if (la.kind == 107) {
+			if (la.kind == 108) {
 				Get();
 				tok = t; arrowKind = 0; 
-			} else if (la.kind == 108) {
+			} else if (la.kind == 109) {
 				Get();
 				tok = t; arrowKind = 1; 
 			} else {
@@ -2436,8 +2427,8 @@ void Formals(bool incoming, bool allowGhostKeyword, bool allowNewKeyword, List<F
 		bool isGhost;
 		bool isOld;
 		
-		Expect(78);
-		if (la.kind == 1 || la.kind == 72 || la.kind == 98) {
+		Expect(79);
+		if (la.kind == 1 || la.kind == 72 || la.kind == 99) {
 			GIdentType(allowGhostKeyword, allowNewKeyword, out id, out ty, out isGhost, out isOld);
 			formals.Add(new Formal(id, id.val, ty, incoming, isGhost, isOld)); 
 			while (la.kind == 26) {
@@ -2446,7 +2437,7 @@ void Formals(bool incoming, bool allowGhostKeyword, bool allowNewKeyword, List<F
 				formals.Add(new Formal(id, id.val, ty, incoming, isGhost, isOld)); 
 			}
 		}
-		Expect(79);
+		Expect(80);
 	}
 
 	void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!*/>/*!*/ mod, List<Expression/*!*/> decreases,
@@ -2456,10 +2447,10 @@ void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!
 		Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
 		IToken lbl = null;
 		
-		while (!(StartOf(15))) {SynErr(192); Get();}
+		while (!(StartOf(15))) {SynErr(193); Get();}
 		if (la.kind == 69) {
 			Get();
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref readsAttrs);
 			}
 			FrameExpression(out fe, false, false);
@@ -2472,7 +2463,7 @@ void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!
 			OldSemi();
 		} else if (la.kind == 68) {
 			Get();
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref modAttrs);
 			}
 			FrameExpression(out fe, false, false);
@@ -2484,13 +2475,13 @@ void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!
 			}
 			OldSemi();
 		} else if (StartOf(16)) {
-			if (la.kind == 105) {
+			if (la.kind == 106) {
 				Get();
 				isFree = true;
 				errors.Deprecated(t, "the 'free' keyword is soon to be deprecated");
 				
 			}
-			if (la.kind == 106) {
+			if (la.kind == 107) {
 				Get();
 				isYield = true; 
 			}
@@ -2511,7 +2502,7 @@ void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!
 				
 			} else if (la.kind == 71) {
 				Get();
-				while (IsAttribute()) {
+				while (la.kind == 74) {
 					Attribute(ref ensAttrs);
 				}
 				Expression(out e, false, false);
@@ -2522,27 +2513,27 @@ void IteratorSpec(List<FrameExpression/*!*/>/*!*/ reads, List<FrameExpression/*!
 				 ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
 				}
 				
-			} else SynErr(193);
+			} else SynErr(194);
 		} else if (la.kind == 44) {
 			Get();
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref decrAttrs);
 			}
 			DecreasesList(decreases, false, false);
 			OldSemi();
-		} else SynErr(194);
+		} else SynErr(195);
 	}
 
 	void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
 		Contract.Ensures(Contract.ValueAtReturn(out block) != null);
 		List<Statement/*!*/> body = new List<Statement/*!*/>();
 		
-		Expect(74);
+		Expect(75);
 		bodyStart = t; 
 		while (StartOf(17)) {
 			Stmt(body);
 		}
-		Expect(75);
+		Expect(76);
 		bodyEnd = t;
 		block = new BlockStmt(bodyStart, bodyEnd, body); 
 	}
@@ -2550,23 +2541,23 @@ void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEn
 	void Variance(out TypeParameter.TPVarianceSyntax variance) {
 		variance = TypeParameter.TPVarianceSyntax.NonVariant_Strict;  // never used; here just to please the C# compiler
 		
-		if (la.kind == 85) {
+		if (la.kind == 86) {
 			Get();
 			variance = TypeParameter.TPVarianceSyntax.Covariant_Permissive; 
-		} else if (la.kind == 101) {
+		} else if (la.kind == 102) {
 			Get();
 			variance = TypeParameter.TPVarianceSyntax.Covariant_Strict; 
-		} else if (la.kind == 102) {
+		} else if (la.kind == 103) {
 			Get();
 			variance = TypeParameter.TPVarianceSyntax.NonVariant_Permissive; 
-		} else if (la.kind == 103) {
+		} else if (la.kind == 104) {
 			Get();
 			variance = TypeParameter.TPVarianceSyntax.Contravariance; 
-		} else SynErr(195);
+		} else SynErr(196);
 	}
 
 	void TPCharOption(ref TypeParameter.TypeParameterCharacteristics characteristics) {
-		if (la.kind == 82) {
+		if (la.kind == 83) {
 			Get();
 			characteristics.EqualitySupport = TypeParameter.EqualitySupportValue.Required; 
 		} else if (la.kind == 2) {
@@ -2577,11 +2568,11 @@ void TPCharOption(ref TypeParameter.TypeParameterCharacteristics characteristics
 			 SemErr(t, "unexpected TPCharOption");
 			}
 			
-		} else if (la.kind == 102) {
+		} else if (la.kind == 103) {
 			Get();
-			Expect(98);
+			Expect(99);
 			characteristics.DisallowReferenceTypes = true; 
-		} else SynErr(196);
+		} else SynErr(197);
 	}
 
 	void FuMe_Ident(out IToken id) {
@@ -2591,19 +2582,19 @@ void FuMe_Ident(out IToken id) {
 		} else if (la.kind == 2) {
 			Get();
 			id = t; 
-		} else SynErr(197);
+		} else SynErr(198);
 	}
 
 	void KType(ref FixpointPredicate.KType kType) {
-		Expect(76);
+		Expect(77);
 		if (la.kind == 11) {
 			Get();
 			kType = FixpointPredicate.KType.Nat; 
 		} else if (la.kind == 13) {
 			Get();
 			kType = FixpointPredicate.KType.ORDINAL; 
-		} else SynErr(198);
-		Expect(77);
+		} else SynErr(199);
+		Expect(78);
 	}
 
 	void MethodSpec(List<MaybeFreeExpression> req, List<FrameExpression> mod, List<MaybeFreeExpression> ens,
@@ -2615,10 +2606,10 @@ void MethodSpec(List<MaybeFreeExpression> req, List<FrameExpression> mod, List<M
 		Expression e;  FrameExpression fe;  bool isFree = false; Attributes ensAttrs = null; Attributes reqAttrs = null;
 		IToken lbl = null;
 		
-		while (!(StartOf(18))) {SynErr(199); Get();}
+		while (!(StartOf(18))) {SynErr(200); Get();}
 		if (la.kind == 68) {
 			Get();
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref modAttrs);
 			}
 			FrameExpression(out fe, false, false);
@@ -2629,8 +2620,8 @@ void MethodSpec(List<MaybeFreeExpression> req, List<FrameExpression> mod, List<M
 				Util.AddFrameExpression(mod, fe, performThisDeprecatedCheck, errors); 
 			}
 			OldSemi();
-		} else if (la.kind == 70 || la.kind == 71 || la.kind == 105) {
-			if (la.kind == 105) {
+		} else if (la.kind == 70 || la.kind == 71 || la.kind == 106) {
+			if (la.kind == 106) {
 				Get();
 				isFree = true;
 				errors.Deprecated(t, "the 'free' keyword is soon to be deprecated");
@@ -2638,7 +2629,7 @@ void MethodSpec(List<MaybeFreeExpression> req, List<FrameExpression> mod, List<M
 			}
 			if (la.kind == 70) {
 				Get();
-				while (IsAttribute()) {
+				while (la.kind == 74) {
 					Attribute(ref reqAttrs);
 				}
 				if (IsLabel(true)) {
@@ -2650,21 +2641,21 @@ void MethodSpec(List<MaybeFreeExpression> req, List<FrameExpression> mod, List<M
 				req.Add(new MaybeFreeExpression(e, isFree, lbl == null ? null : new AssertLabel(lbl, lbl.val), reqAttrs)); 
 			} else if (la.kind == 71) {
 				Get();
-				while (IsAttribute()) {
+				while (la.kind == 74) {
 					Attribute(ref ensAttrs);
 				}
 				Expression(out e, false, false);
 				OldSemi();
 				ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); 
-			} else SynErr(200);
+			} else SynErr(201);
 		} else if (la.kind == 44) {
 			Get();
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref decAttrs);
 			}
 			DecreasesList(decreases, true, false);
 			OldSemi();
-		} else SynErr(201);
+		} else SynErr(202);
 	}
 
 	void DividedBlockStmt(out DividedBlockStmt body, out IToken bodyStart, out IToken bodyEnd) {
@@ -2673,12 +2664,12 @@ void DividedBlockStmt(out DividedBlockStmt body, out IToken bodyStart, out IToke
 		IToken separatorTok = null;
 		List<Statement> bodyProper = new List<Statement>();
 		
-		Expect(74);
+		Expect(75);
 		bodyStart = t; 
 		while (StartOf(17)) {
 			Stmt(bodyInit);
 		}
-		if (la.kind == 98) {
+		if (la.kind == 99) {
 			Get();
 			separatorTok = t; 
 			Expect(34);
@@ -2686,7 +2677,7 @@ void DividedBlockStmt(out DividedBlockStmt body, out IToken bodyStart, out IToke
 				Stmt(bodyProper);
 			}
 		}
-		Expect(75);
+		Expect(76);
 		bodyEnd = t; 
 		body = new DividedBlockStmt(bodyStart, bodyEnd, bodyInit, separatorTok, bodyProper); 
 	}
@@ -2712,7 +2703,7 @@ void FrameExpression(out FrameExpression fe, bool allowSemi, bool allowLambda) {
 			Ident(out id);
 			fieldName = id.val; 
 			fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); 
-		} else SynErr(202);
+		} else SynErr(203);
 	}
 
 	void LabelIdent(out IToken id) {
@@ -2722,7 +2713,7 @@ void LabelIdent(out IToken id) {
 		} else if (la.kind == 2) {
 			Get();
 			id = t; 
-		} else SynErr(203);
+		} else SynErr(204);
 	}
 
 	void DecreasesList(List<Expression> decreases, bool allowWildcard, bool allowLambda) {
@@ -2764,7 +2755,7 @@ void NameSegmentForTypeName(out Expression e, bool inExpressionContext) {
 
 	void GenericInstantiation(List<Type> gt) {
 		Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; 
-		Expect(80);
+		Expect(81);
 		Type(out ty);
 		gt.Add(ty); 
 		while (la.kind == 26) {
@@ -2772,7 +2763,7 @@ void GenericInstantiation(List<Type> gt) {
 			Type(out ty);
 			gt.Add(ty); 
 		}
-		Expect(81);
+		Expect(82);
 	}
 
 	void FunctionSpec(List<MaybeFreeExpression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<MaybeFreeExpression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -2781,10 +2772,10 @@ void FunctionSpec(List<MaybeFreeExpression/*!*/>/*!*/ reqs, List<FrameExpression
 		Contract.Requires(decreases == null || cce.NonNullElements(decreases));
 		Expression/*!*/ e;  FrameExpression/*!*/ fe;
 		Attributes ensAttrs = null; Attributes reqAttrs = null; 
-		while (!(StartOf(19))) {SynErr(204); Get();}
+		while (!(StartOf(19))) {SynErr(205); Get();}
 		if (la.kind == 70) {
 			Get();
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref reqAttrs);
 			}
 			Expression(out e, false, false);
@@ -2802,7 +2793,7 @@ void FunctionSpec(List<MaybeFreeExpression/*!*/>/*!*/ reqs, List<FrameExpression
 			OldSemi();
 		} else if (la.kind == 71) {
 			Get();
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref ensAttrs);
 			}
 			Expression(out e, false, false);
@@ -2817,37 +2808,37 @@ void FunctionSpec(List<MaybeFreeExpression/*!*/>/*!*/ reqs, List<FrameExpression
 			
 			DecreasesList(decreases, false, false);
 			OldSemi();
-		} else SynErr(205);
+		} else SynErr(206);
 	}
 
 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 
-		Expect(74);
+		Expect(75);
 		bodyStart = t; 
 		Expression(out e, true, true);
-		Expect(75);
+		Expect(76);
 		bodyEnd = t; 
 	}
 
 	void PossiblyWildFrameExpression(out FrameExpression fe, bool allowSemi) {
 		Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; 
-		if (la.kind == 85) {
+		if (la.kind == 86) {
 			Get();
 			fe = new FrameExpression(t, new WildcardExpr(t), null); 
 		} else if (StartOf(20)) {
 			FrameExpression(out fe, allowSemi, false);
-		} else SynErr(206);
+		} else SynErr(207);
 	}
 
 	void PossiblyWildExpression(out Expression e, bool allowLambda) {
 		Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
 		e = dummyExpr; 
-		if (la.kind == 85) {
+		if (la.kind == 86) {
 			Get();
 			e = new WildcardExpr(t); 
 		} else if (StartOf(8)) {
 			Expression(out e, false, allowLambda);
-		} else SynErr(207);
+		} else SynErr(208);
 	}
 
 	void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -2864,14 +2855,14 @@ void OneStmt(out Statement/*!*/ s) {
 		IToken bodyStart, bodyEnd;
 		int breakCount;
 		
-		while (!(StartOf(21))) {SynErr(208); Get();}
+		while (!(StartOf(21))) {SynErr(209); Get();}
 		switch (la.kind) {
-		case 74: {
+		case 75: {
 			BlockStmt(out bs, out bodyStart, out bodyEnd);
 			s = bs; 
 			break;
 		}
-		case 117: {
+		case 118: {
 			AssertStmt(out s, false);
 			break;
 		}
@@ -2879,15 +2870,15 @@ void OneStmt(out Statement/*!*/ s) {
 			AssumeStmt(out s);
 			break;
 		}
-		case 118: {
+		case 119: {
 			PrintStmt(out s);
 			break;
 		}
-		case 88: {
+		case 89: {
 			RevealStmt(out s);
 			break;
 		}
-		case 1: case 2: case 3: case 4: case 10: case 12: case 23: case 24: case 27: case 78: case 145: case 146: case 147: case 148: case 149: case 150: case 151: case 153: {
+		case 1: case 2: case 3: case 4: case 10: case 12: case 23: case 24: case 27: case 79: case 146: case 147: case 148: case 149: case 150: case 151: case 152: case 154: {
 			UpdateStmt(out s);
 			break;
 		}
@@ -2895,19 +2886,19 @@ void OneStmt(out Statement/*!*/ s) {
 			VarDeclStatement(out s);
 			break;
 		}
-		case 114: {
+		case 115: {
 			IfStmt(out s);
 			break;
 		}
-		case 115: {
+		case 116: {
 			WhileStmt(out s);
 			break;
 		}
-		case 116: {
+		case 117: {
 			MatchStmt(out s);
 			break;
 		}
-		case 119: case 120: {
+		case 120: case 121: {
 			ForallStmt(out s);
 			break;
 		}
@@ -2915,11 +2906,11 @@ void OneStmt(out Statement/*!*/ s) {
 			CalcStmt(out s);
 			break;
 		}
-		case 121: {
+		case 122: {
 			ModifyStmt(out s);
 			break;
 		}
-		case 110: {
+		case 111: {
 			Get();
 			LabelIdent(out id);
 			Expect(25);
@@ -2927,32 +2918,32 @@ void OneStmt(out Statement/*!*/ s) {
 			s.Labels = new LList<Label>(new Label(id, id.val), s.Labels); 
 			break;
 		}
-		case 111: {
+		case 112: {
 			Get();
 			x = t; breakCount = 1; label = null; 
 			if (la.kind == 1 || la.kind == 2) {
 				LabelIdent(out id);
 				label = id.val; 
-			} else if (la.kind == 34 || la.kind == 111) {
-				while (la.kind == 111) {
+			} else if (la.kind == 34 || la.kind == 112) {
+				while (la.kind == 112) {
 					Get();
 					breakCount++; 
 				}
-			} else SynErr(209);
-			while (!(la.kind == 0 || la.kind == 34)) {SynErr(210); Get();}
+			} else SynErr(210);
+			while (!(la.kind == 0 || la.kind == 34)) {SynErr(211); Get();}
 			Expect(34);
 			s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount); 
 			break;
 		}
-		case 106: case 113: {
+		case 107: case 114: {
 			ReturnStmt(out s);
 			break;
 		}
-		case 87: {
+		case 88: {
 			SkeletonStmt(out s);
 			break;
 		}
-		default: SynErr(211); break;
+		default: SynErr(212); break;
 		}
 	}
 
@@ -2964,9 +2955,9 @@ void AssertStmt(out Statement/*!*/ s, bool inExprContext) {
 		IToken proofStart, proofEnd;
 		IToken lbl = null;
 		
-		Expect(117);
+		Expect(118);
 		x = t; 
-		while (IsAttribute()) {
+		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		if (StartOf(8)) {
@@ -2980,12 +2971,12 @@ void AssertStmt(out Statement/*!*/ s, bool inExprContext) {
 				BlockStmt(out proof, out proofStart, out proofEnd);
 			} else if (la.kind == 34) {
 				Get();
-			} else SynErr(212);
-		} else if (la.kind == 87) {
+			} else SynErr(213);
+		} else if (la.kind == 88) {
 			Get();
 			dotdotdot = t; 
 			Expect(34);
-		} else SynErr(213);
+		} else SynErr(214);
 		if (dotdotdot != null) {
 		 s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), null, null, attrs), dotdotdot, null);
 		} else {
@@ -3001,15 +2992,15 @@ void AssumeStmt(out Statement/*!*/ s) {
 		
 		Expect(36);
 		x = t; 
-		while (IsAttribute()) {
+		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		if (StartOf(8)) {
 			Expression(out e, false, true);
-		} else if (la.kind == 87) {
+		} else if (la.kind == 88) {
 			Get();
 			dotdotdot = t; 
-		} else SynErr(214);
+		} else SynErr(215);
 		Expect(34);
 		if (dotdotdot != null) {
 		 s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -3024,7 +3015,7 @@ void PrintStmt(out Statement s) {
 		IToken x;  Expression e;
 		var args = new List<Expression>();
 		
-		Expect(118);
+		Expect(119);
 		x = t; 
 		Expression(out e, false, true);
 		args.Add(e); 
@@ -3041,7 +3032,7 @@ void RevealStmt(out Statement s) {
 		Contract.Ensures(Contract.ValueAtReturn(out s) != null);
 		IToken x; Expression e; var es = new List<Expression>();
 		
-		Expect(88);
+		Expect(89);
 		x = t; 
 		Expression(out e, false, true);
 		es.Add(e); 
@@ -3096,13 +3087,13 @@ void UpdateStmt(out Statement/*!*/ s) {
 					suchThatAssume = t; 
 				}
 				Expression(out suchThat, false, true);
-			} else SynErr(215);
+			} else SynErr(216);
 			Expect(34);
 			endTok = t; 
 		} else if (la.kind == 25) {
 			Get();
 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 
-		} else SynErr(216);
+		} else SynErr(217);
 		if (suchThat != null) {
 		 s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume, null);
 		} else {
@@ -3171,7 +3162,7 @@ void VarDeclStatement(out Statement/*!*/ s) {
 					Expression(out suchThat, false, true);
 				}
 			}
-			while (!(la.kind == 0 || la.kind == 34)) {SynErr(217); Get();}
+			while (!(la.kind == 0 || la.kind == 34)) {SynErr(218); Get();}
 			Expect(34);
 			endTok = t; 
 			ConcreteUpdateStatement update;
@@ -3192,7 +3183,7 @@ void VarDeclStatement(out Statement/*!*/ s) {
 			}
 			s = new VarDeclStmt(x, endTok, lhss, update);
 			
-		} else if (la.kind == 1 || la.kind == 78) {
+		} else if (la.kind == 1 || la.kind == 79) {
 			CasePattern<LocalVariable> pat;
 			Expression e = dummyExpr;
 			IToken id = t;
@@ -3206,11 +3197,11 @@ void VarDeclStatement(out Statement/*!*/ s) {
 				}
 				Expect(30);
 				SemErr(pat.tok, "LHS of assign-such-that expression must be variables, not general patterns"); 
-			} else SynErr(218);
+			} else SynErr(219);
 			Expression(out e, false, true);
 			Expect(34);
 			s = new LetStmt(e.tok, e.tok, pat, e); 
-		} else SynErr(219);
+		} else SynErr(220);
 	}
 
 	void IfStmt(out Statement/*!*/ ifStmt) {
@@ -3225,7 +3216,7 @@ void IfStmt(out Statement/*!*/ ifStmt) {
 		ifStmt = dummyIfStmt;  // to please the compiler
 		bool usesOptionalBraces;
 		
-		Expect(114);
+		Expect(115);
 		x = t; 
 		if (IsAlternative()) {
 			AlternativeBlock(true, out alternatives, out usesOptionalBraces, out endTok);
@@ -3244,13 +3235,13 @@ void IfStmt(out Statement/*!*/ ifStmt) {
 			endTok = thn.EndTok; 
 			if (la.kind == 40) {
 				Get();
-				if (la.kind == 114) {
+				if (la.kind == 115) {
 					IfStmt(out s);
 					els = s; endTok = s.EndTok; 
-				} else if (la.kind == 74) {
+				} else if (la.kind == 75) {
 					BlockStmt(out bs, out bodyStart, out bodyEnd);
 					els = bs; endTok = bs.EndTok; 
-				} else SynErr(220);
+				} else SynErr(221);
 			}
 			if (guardEllipsis != null) {
 			 ifStmt = new SkeletonStatement(new IfStmt(x, endTok, isExistentialGuard, guard, thn, els), guardEllipsis, null);
@@ -3258,7 +3249,7 @@ void IfStmt(out Statement/*!*/ ifStmt) {
 			 ifStmt = new IfStmt(x, endTok, isExistentialGuard, guard, thn, els);
 			}
 			
-		} else SynErr(221);
+		} else SynErr(222);
 	}
 
 	void WhileStmt(out Statement stmt) {
@@ -3278,7 +3269,7 @@ void WhileStmt(out Statement stmt) {
 		bool isDirtyLoop = true;
 		bool usesOptionalBraces;
 		
-		Expect(115);
+		Expect(116);
 		x = t; 
 		if (IsLoopSpec() || IsAlternative()) {
 			while (StartOf(24)) {
@@ -3301,10 +3292,10 @@ void WhileStmt(out Statement stmt) {
 				BlockStmt(out body, out bodyStart, out bodyEnd);
 				endTok = body.EndTok; isDirtyLoop = false; 
 			} else if (la.kind == _ellipsis) {
-				Expect(87);
+				Expect(88);
 				bodyEllipsis = t; endTok = t; isDirtyLoop = false; 
 			} else if (StartOf(25)) {
-			} else SynErr(222);
+			} else SynErr(223);
 			if (guardEllipsis != null || bodyEllipsis != null) {
 			 if (mod != null) {
 			   SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -3322,7 +3313,7 @@ void WhileStmt(out Statement stmt) {
 			 stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
 			}
 			
-		} else SynErr(223);
+		} else SynErr(224);
 	}
 
 	void MatchStmt(out Statement/*!*/ s) {
@@ -3331,23 +3322,23 @@ void MatchStmt(out Statement/*!*/ s) {
 		List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
 		bool usesOptionalBraces = false;
 		
-		Expect(116);
+		Expect(117);
 		x = t; 
 		Expression(out e, true, true);
 		if (la.kind == _lbrace) {
-			Expect(74);
+			Expect(75);
 			usesOptionalBraces = true; 
 			while (la.kind == 38) {
 				CaseStatement(out c);
 				cases.Add(c); 
 			}
-			Expect(75);
+			Expect(76);
 		} else if (StartOf(25)) {
 			while (la.kind == _case) {
 				CaseStatement(out c);
 				cases.Add(c); 
 			}
-		} else SynErr(224);
+		} else SynErr(225);
 		s = new MatchStmt(x, t, e, cases, usesOptionalBraces); 
 	}
 
@@ -3364,32 +3355,32 @@ void ForallStmt(out Statement/*!*/ s) {
 		IToken bodyStart, bodyEnd;
 		IToken tok = Token.NoToken;
 		
-		if (la.kind == 119) {
+		if (la.kind == 120) {
 			Get();
 			x = t; tok = x; 
-		} else if (la.kind == 120) {
+		} else if (la.kind == 121) {
 			Get();
 			x = t;
 			errors.Deprecated(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
 			
-		} else SynErr(225);
+		} else SynErr(226);
 		if (la.kind == _openparen) {
-			Expect(78);
+			Expect(79);
 			if (la.kind == 1) {
 				QuantifierDomain(out bvars, out attrs, out range);
 			}
-			Expect(79);
+			Expect(80);
 		} else if (StartOf(26)) {
 			if (la.kind == _ident) {
 				QuantifierDomain(out bvars, out attrs, out range);
 			}
-		} else SynErr(226);
+		} else SynErr(227);
 		if (bvars == null) { bvars = new List<BoundVar>(); }
 		if (range == null) { range = new LiteralExpr(x, true); }
 		
-		while (la.kind == 71 || la.kind == 105) {
+		while (la.kind == 71 || la.kind == 106) {
 			isFree = false; 
-			if (la.kind == 105) {
+			if (la.kind == 106) {
 				Get();
 				isFree = true;
 				errors.Deprecated(t, "the 'free' keyword is soon to be deprecated");
@@ -3430,7 +3421,7 @@ void CalcStmt(out Statement s) {
 		
 		Expect(37);
 		x = t; 
-		while (IsAttribute()) {
+		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		if (StartOf(27)) {
@@ -3442,7 +3433,7 @@ void CalcStmt(out Statement s) {
 			}
 			
 		}
-		Expect(74);
+		Expect(75);
 		while (StartOf(8)) {
 			Expression(out e, false, true);
 			lines.Add(e); stepOp = null; danglingOperator = null; 
@@ -3466,20 +3457,20 @@ void CalcStmt(out Statement s) {
 			BlockStmt subBlock; Statement subCalc;
 			
 			while (la.kind == _lbrace || la.kind == _calc) {
-				if (la.kind == 74) {
+				if (la.kind == 75) {
 					BlockStmt(out subBlock, out t0, out t1);
 					hintEnd = subBlock.EndTok; subhints.Add(subBlock); 
 				} else if (la.kind == 37) {
 					CalcStmt(out subCalc);
 					hintEnd = subCalc.EndTok; subhints.Add(subCalc); 
-				} else SynErr(227);
+				} else SynErr(228);
 			}
 			var h = new BlockStmt(hintStart, hintEnd, subhints); // if the hint is empty, hintStart is the first token of the next line, but it doesn't matter because the block statement is just used as a container
 			hints.Add(h);
 			if (h.Body.Count != 0) { danglingOperator = null; }
 			
 		}
-		Expect(75);
+		Expect(76);
 		if (danglingOperator != null) {
 		 SemErr(danglingOperator, "a calculation cannot end with an operator");
 		}
@@ -3498,9 +3489,9 @@ void ModifyStmt(out Statement s) {
 		BlockStmt body = null;  IToken bodyStart;
 		IToken ellipsisToken = null;
 		
-		Expect(121);
+		Expect(122);
 		tok = t; 
-		while (IsAttribute()) {
+		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		if (StartOf(20)) {
@@ -3511,17 +3502,17 @@ void ModifyStmt(out Statement s) {
 				FrameExpression(out fe, false, true);
 				mod.Add(fe); 
 			}
-		} else if (la.kind == 87) {
+		} else if (la.kind == 88) {
 			Get();
 			ellipsisToken = t; 
-		} else SynErr(228);
-		if (la.kind == 74) {
+		} else SynErr(229);
+		if (la.kind == 75) {
 			BlockStmt(out body, out bodyStart, out endTok);
 		} else if (la.kind == 34) {
-			while (!(la.kind == 0 || la.kind == 34)) {SynErr(229); Get();}
+			while (!(la.kind == 0 || la.kind == 34)) {SynErr(230); Get();}
 			Get();
 			endTok = t; 
-		} else SynErr(230);
+		} else SynErr(231);
 		s = new ModifyStmt(tok, endTok, mod, attrs, body);
 		if (ellipsisToken != null) {
 		 s = new SkeletonStatement(s, ellipsisToken, null);
@@ -3535,13 +3526,13 @@ void ReturnStmt(out Statement/*!*/ s) {
 		AssignmentRhs r;
 		bool isYield = false;
 		
-		if (la.kind == 113) {
+		if (la.kind == 114) {
 			Get();
 			returnTok = t; 
-		} else if (la.kind == 106) {
+		} else if (la.kind == 107) {
 			Get();
 			returnTok = t; isYield = true; 
-		} else SynErr(231);
+		} else SynErr(232);
 		if (StartOf(28)) {
 			Rhs(out r);
 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 
@@ -3565,9 +3556,9 @@ void SkeletonStmt(out Statement s) {
 		List<Expression> exprs = null;
 		IToken tok, dotdotdot, whereTok;
 		Expression e; 
-		Expect(87);
+		Expect(88);
 		dotdotdot = t; 
-		if (la.kind == 112) {
+		if (la.kind == 113) {
 			Get();
 			names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
 			Ident(out tok);
@@ -3606,15 +3597,15 @@ void Rhs(out AssignmentRhs r) {
 		r = dummyRhs;  // to please compiler
 		Attributes attrs = null;
 		
-		if (la.kind == 98) {
+		if (la.kind == 99) {
 			Get();
 			newToken = t; 
-			if (la.kind == 76) {
+			if (la.kind == 77) {
 				NewArray(out ee, out arrayElementInit, out display);
 			} else if (StartOf(5)) {
 				TypeAndToken(out x, out ty, false);
-				if (la.kind == 76 || la.kind == 78) {
-					if (la.kind == 76) {
+				if (la.kind == 77 || la.kind == 79) {
+					if (la.kind == 77) {
 						NewArray(out ee, out arrayElementInit, out display);
 					} else {
 						x = null; args = new List<Expression/*!*/>(); 
@@ -3622,10 +3613,10 @@ void Rhs(out AssignmentRhs r) {
 						if (StartOf(8)) {
 							Expressions(args);
 						}
-						Expect(79);
+						Expect(80);
 					}
 				}
-			} else SynErr(232);
+			} else SynErr(233);
 			if (ee != null) {
 			 if (display != null) {
 			   r = new TypeRhs(newToken, ty, ee[0], display);
@@ -3638,13 +3629,13 @@ void Rhs(out AssignmentRhs r) {
 			 r = new TypeRhs(newToken, ty);
 			}
 			
-		} else if (la.kind == 85) {
+		} else if (la.kind == 86) {
 			Get();
 			r = new HavocRhs(t); 
 		} else if (StartOf(8)) {
 			Expression(out e, false, true);
 			r = new ExprRhs(e); 
-		} else SynErr(233);
+		} else SynErr(234);
 		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
@@ -3656,16 +3647,16 @@ void Lhs(out Expression e) {
 		
 		if (la.kind == 1) {
 			NameSegment(out e);
-			while (la.kind == 32 || la.kind == 76 || la.kind == 78) {
+			while (la.kind == 32 || la.kind == 77 || la.kind == 79) {
 				Suffix(ref e);
 			}
 		} else if (StartOf(29)) {
 			ConstAtomExpression(out e, false, false);
 			Suffix(ref e);
-			while (la.kind == 32 || la.kind == 76 || la.kind == 78) {
+			while (la.kind == 32 || la.kind == 77 || la.kind == 79) {
 				Suffix(ref e);
 			}
-		} else SynErr(234);
+		} else SynErr(235);
 	}
 
 	void NewArray(out List<Expression> ee, out Expression arrayElementInit, out List<Expression> display ) {
@@ -3674,28 +3665,28 @@ void NewArray(out List<Expression> ee, out Expression arrayElementInit, out List
 		display = null;
 		IToken x;
 		
-		Expect(76);
+		Expect(77);
 		x = t; 
-		if (la.kind == 77) {
+		if (la.kind == 78) {
 			Get();
-			Expect(76);
+			Expect(77);
 			display = new List<Expression>(); 
 			if (StartOf(8)) {
 				Expressions(display);
 			}
-			Expect(77);
+			Expect(78);
 			ee.Add(new LiteralExpr(x, display.Count));
 			
 		} else if (StartOf(8)) {
 			Expressions(ee);
-			Expect(77);
+			Expect(78);
 			var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
 			
-			if (la.kind == 76 || la.kind == 78) {
-				if (la.kind == 78) {
+			if (la.kind == 77 || la.kind == 79) {
+				if (la.kind == 79) {
 					Get();
 					Expression(out arrayElementInit, true, true);
-					Expect(79);
+					Expect(80);
 				} else {
 					Get();
 					if (ee.Count > 1) {
@@ -3706,10 +3697,10 @@ void NewArray(out List<Expression> ee, out Expression arrayElementInit, out List
 					if (StartOf(8)) {
 						Expressions(display);
 					}
-					Expect(77);
+					Expect(78);
 				}
 			}
-		} else SynErr(235);
+		} else SynErr(236);
 		if (ee.Count == 0) {
 		 // an error occurred while parsing, but we still want to make sure to return a nonempty "ee"
 		 ee.Add(new LiteralExpr(x, 0));
@@ -3735,9 +3726,9 @@ void CasePatternLocal(out CasePattern<LocalVariable> pat, bool isGhost) {
 		
 		if (IsIdentParen()) {
 			Ident(out id);
-			Expect(78);
+			Expect(79);
 			arguments = new List<CasePattern<LocalVariable>>(); 
-			if (la.kind == 1 || la.kind == 78) {
+			if (la.kind == 1 || la.kind == 79) {
 				CasePatternLocal(out pat, isGhost);
 				arguments.Add(pat); 
 				while (la.kind == 26) {
@@ -3746,14 +3737,14 @@ void CasePatternLocal(out CasePattern<LocalVariable> pat, bool isGhost) {
 					arguments.Add(pat); 
 				}
 			}
-			Expect(79);
+			Expect(80);
 			pat = new CasePattern<LocalVariable>(id, id.val, arguments); 
-		} else if (la.kind == 78) {
+		} else if (la.kind == 79) {
 			Get();
 			id = t;
 			arguments = new List<CasePattern<LocalVariable>>();
 			
-			if (la.kind == 1 || la.kind == 78) {
+			if (la.kind == 1 || la.kind == 79) {
 				CasePatternLocal(out pat, isGhost);
 				arguments.Add(pat); 
 				while (la.kind == 26) {
@@ -3762,7 +3753,7 @@ void CasePatternLocal(out CasePattern<LocalVariable> pat, bool isGhost) {
 					arguments.Add(pat); 
 				}
 			}
-			Expect(79);
+			Expect(80);
 			theBuiltIns.TupleType(id, arguments.Count, true); // make sure the tuple type exists
 			string ctor = BuiltIns.TupleTypeCtorNamePrefix + arguments.Count;  //use the TupleTypeCtors
 			pat = new CasePattern<LocalVariable>(id, ctor, arguments);
@@ -3771,7 +3762,7 @@ void CasePatternLocal(out CasePattern<LocalVariable> pat, bool isGhost) {
 			LocalIdentTypeOptional(out local, isGhost);
 			pat = new CasePattern<LocalVariable>(local.Tok, local);
 			
-		} else SynErr(236);
+		} else SynErr(237);
 		if (pat == null) {
 		 pat = new CasePattern<LocalVariable>(t, "_ParseError", new List<CasePattern<LocalVariable>>());
 		}
@@ -3784,14 +3775,14 @@ void AlternativeBlock(bool allowExistentialGuards, out List<GuardedAlternative>
 		usesOptionalBraces = false;
 		GuardedAlternative alt;
 		
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			Get();
 			usesOptionalBraces = true; 
 			while (la.kind == 38) {
 				AlternativeBlockCase(allowExistentialGuards, out alt);
 				alternatives.Add(alt); 
 			}
-			Expect(75);
+			Expect(76);
 		} else if (la.kind == 38) {
 			AlternativeBlockCase(allowExistentialGuards, out alt);
 			alternatives.Add(alt); 
@@ -3799,7 +3790,7 @@ void AlternativeBlock(bool allowExistentialGuards, out List<GuardedAlternative>
 				AlternativeBlockCase(allowExistentialGuards, out alt);
 				alternatives.Add(alt); 
 			}
-		} else SynErr(237);
+		} else SynErr(238);
 		endTok = t; 
 	}
 
@@ -3826,18 +3817,18 @@ void ExistentialGuard(out Expression e, bool allowLambda) {
 
 	void Guard(out Expression e) {
 		Expression/*!*/ ee;  e = null; 
-		if (la.kind == 85) {
+		if (la.kind == 86) {
 			Get();
 			e = null; 
 		} else if (IsParenStar()) {
-			Expect(78);
-			Expect(85);
 			Expect(79);
+			Expect(86);
+			Expect(80);
 			e = null; 
 		} else if (StartOf(8)) {
 			Expression(out ee, true, true);
 			e = ee; 
-		} else SynErr(238);
+		} else SynErr(239);
 	}
 
 	void AlternativeBlockCase(bool allowExistentialGuards, out GuardedAlternative alt) {
@@ -3852,13 +3843,13 @@ void AlternativeBlockCase(bool allowExistentialGuards, out GuardedAlternative al
 			isExistentialGuard = true; 
 		} else if (StartOf(8)) {
 			Expression(out e, true, false);
-		} else SynErr(239);
+		} else SynErr(240);
 		Expect(35);
 		body = new List<Statement>(); 
-		while (!(StartOf(30))) {SynErr(240); Get();}
+		while (!(StartOf(30))) {SynErr(241); Get();}
 		while (IsNotEndOfCase()) {
 			Stmt(body);
-			while (!(StartOf(30))) {SynErr(241); Get();}
+			while (!(StartOf(30))) {SynErr(242); Get();}
 		}
 		alt = new GuardedAlternative(x, isExistentialGuard, e, body); 
 	}
@@ -3867,32 +3858,32 @@ void LoopSpec(List<MaybeFreeExpression> invariants, List<Expression> decreases,
 		Expression e; FrameExpression fe;
 		bool isFree = false; Attributes attrs = null;
 		
-		if (la.kind == 45 || la.kind == 105) {
-			while (!(la.kind == 0 || la.kind == 45 || la.kind == 105)) {SynErr(242); Get();}
-			if (la.kind == 105) {
+		if (la.kind == 45 || la.kind == 106) {
+			while (!(la.kind == 0 || la.kind == 45 || la.kind == 106)) {SynErr(243); Get();}
+			if (la.kind == 106) {
 				Get();
 				isFree = true; errors.Deprecated(t, "the 'free' keyword is soon to be deprecated"); 
 			}
 			Expect(45);
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref attrs);
 			}
 			Expression(out e, false, true);
 			invariants.Add(new MaybeFreeExpression(e, isFree, attrs)); 
 			OldSemi();
 		} else if (la.kind == 44) {
-			while (!(la.kind == 0 || la.kind == 44)) {SynErr(243); Get();}
+			while (!(la.kind == 0 || la.kind == 44)) {SynErr(244); Get();}
 			Get();
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref decAttrs);
 			}
 			DecreasesList(decreases, true, true);
 			OldSemi();
 		} else if (la.kind == 68) {
-			while (!(la.kind == 0 || la.kind == 68)) {SynErr(244); Get();}
+			while (!(la.kind == 0 || la.kind == 68)) {SynErr(245); Get();}
 			Get();
 			mod = mod ?? new List<FrameExpression>(); 
-			while (IsAttribute()) {
+			while (la.kind == 74) {
 				Attribute(ref modAttrs);
 			}
 			FrameExpression(out fe, false, true);
@@ -3903,7 +3894,7 @@ void LoopSpec(List<MaybeFreeExpression> invariants, List<Expression> decreases,
 				mod.Add(fe); 
 			}
 			OldSemi();
-		} else SynErr(245);
+		} else SynErr(246);
 	}
 
 	void CaseStatement(out MatchCaseStmt/*!*/ c) {
@@ -3919,9 +3910,9 @@ void CaseStatement(out MatchCaseStmt/*!*/ c) {
 		if (la.kind == 1) {
 			Ident(out id);
 			name = id.val; 
-			if (la.kind == 78) {
+			if (la.kind == 79) {
 				Get();
-				if (la.kind == 1 || la.kind == 78) {
+				if (la.kind == 1 || la.kind == 79) {
 					CasePattern(out pat);
 					arguments.Add(pat); 
 					while (la.kind == 26) {
@@ -3930,9 +3921,9 @@ void CaseStatement(out MatchCaseStmt/*!*/ c) {
 						arguments.Add(pat); 
 					}
 				}
-				Expect(79);
+				Expect(80);
 			}
-		} else if (la.kind == 78) {
+		} else if (la.kind == 79) {
 			Get();
 			CasePattern(out pat);
 			arguments.Add(pat); 
@@ -3941,13 +3932,13 @@ void CaseStatement(out MatchCaseStmt/*!*/ c) {
 				CasePattern(out pat);
 				arguments.Add(pat); 
 			}
-			Expect(79);
-		} else SynErr(246);
+			Expect(80);
+		} else SynErr(247);
 		Expect(35);
-		while (!(StartOf(30))) {SynErr(247); Get();}
+		while (!(StartOf(30))) {SynErr(248); Get();}
 		while (IsNotEndOfCase()) {
 			Stmt(body);
-			while (!(StartOf(30))) {SynErr(248); Get();}
+			while (!(StartOf(30))) {SynErr(249); Get();}
 		}
 		c = new MatchCaseStmt(x, name, arguments, body); 
 	}
@@ -3959,9 +3950,9 @@ void CasePattern(out CasePattern<BoundVar> pat) {
 		
 		if (IsIdentParen()) {
 			Ident(out id);
-			Expect(78);
+			Expect(79);
 			arguments = new List<CasePattern<BoundVar>>(); 
-			if (la.kind == 1 || la.kind == 78) {
+			if (la.kind == 1 || la.kind == 79) {
 				CasePattern(out pat);
 				arguments.Add(pat); 
 				while (la.kind == 26) {
@@ -3970,14 +3961,14 @@ void CasePattern(out CasePattern<BoundVar> pat) {
 					arguments.Add(pat); 
 				}
 			}
-			Expect(79);
+			Expect(80);
 			pat = new CasePattern<BoundVar>(id, id.val, arguments); 
-		} else if (la.kind == 78) {
+		} else if (la.kind == 79) {
 			Get();
 			id = t;
 			arguments = new List<CasePattern<BoundVar>>();
 			
-			if (la.kind == 1 || la.kind == 78) {
+			if (la.kind == 1 || la.kind == 79) {
 				CasePattern(out pat);
 				arguments.Add(pat); 
 				while (la.kind == 26) {
@@ -3986,7 +3977,7 @@ void CasePattern(out CasePattern<BoundVar> pat) {
 					arguments.Add(pat); 
 				}
 			}
-			Expect(79);
+			Expect(80);
 			theBuiltIns.TupleType(id, arguments.Count, true); // make sure the tuple type exists
 			string ctor = BuiltIns.TupleTypeCtorNamePrefix + arguments.Count;  //use the TupleTypeCtors
 			pat = new CasePattern<BoundVar>(id, ctor, arguments);
@@ -3995,7 +3986,7 @@ void CasePattern(out CasePattern<BoundVar> pat) {
 			IdentTypeOptional(out bv);
 			pat = new CasePattern<BoundVar>(bv.tok, bv);
 			
-		} else SynErr(249);
+		} else SynErr(250);
 		if (pat == null) {
 		 pat = new CasePattern<BoundVar>(t, "_ParseError", new List<CasePattern<BoundVar>>());
 		}
@@ -4015,7 +4006,7 @@ void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expres
 			IdentTypeOptional(out bv);
 			bvars.Add(bv); 
 		}
-		while (IsAttribute()) {
+		while (la.kind == 74) {
 			Attribute(ref attrs);
 		}
 		if (la.kind == _verticalbar) {
@@ -4030,73 +4021,73 @@ void CalcOp(out IToken x, out CalcStmt.CalcOp/*!*/ op) {
 		x = null;
 		
 		switch (la.kind) {
-		case 82: {
+		case 83: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Eq; 
-			if (la.kind == 122) {
+			if (la.kind == 123) {
 				Get();
-				Expect(76);
-				Expression(out k, true, true);
 				Expect(77);
+				Expression(out k, true, true);
+				Expect(78);
 			}
 			break;
 		}
-		case 80: {
+		case 81: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Lt; 
 			break;
 		}
-		case 81: {
+		case 82: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Gt; 
 			break;
 		}
-		case 123: {
+		case 124: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 124: {
+		case 125: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		case 83: {
+		case 84: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 84: {
+		case 85: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 125: {
+		case 126: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 126: {
+		case 127: {
 			Get();
 			x = t;  binOp = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		case 127: case 128: {
+		case 128: case 129: {
 			EquivOp();
 			x = t;  binOp = BinaryExpr.Opcode.Iff; 
 			break;
 		}
-		case 129: case 130: {
+		case 130: case 131: {
 			ImpliesOp();
 			x = t;  binOp = BinaryExpr.Opcode.Imp; 
 			break;
 		}
-		case 131: case 132: {
+		case 132: case 133: {
 			ExpliesOp();
 			x = t;  binOp = BinaryExpr.Opcode.Exp; 
 			break;
 		}
-		default: SynErr(250); break;
+		default: SynErr(251); break;
 		}
 		if (k == null) {
 		 op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -4107,67 +4098,67 @@ void CalcOp(out IToken x, out CalcStmt.CalcOp/*!*/ op) {
 	}
 
 	void EquivOp() {
-		if (la.kind == 127) {
+		if (la.kind == 128) {
 			Get();
-		} else if (la.kind == 128) {
+		} else if (la.kind == 129) {
 			Get();
-		} else SynErr(251);
+		} else SynErr(252);
 	}
 
 	void ImpliesOp() {
-		if (la.kind == 129) {
+		if (la.kind == 130) {
 			Get();
-		} else if (la.kind == 130) {
+		} else if (la.kind == 131) {
 			Get();
-		} else SynErr(252);
+		} else SynErr(253);
 	}
 
 	void ExpliesOp() {
-		if (la.kind == 131) {
+		if (la.kind == 132) {
 			Get();
-		} else if (la.kind == 132) {
+		} else if (la.kind == 133) {
 			Get();
-		} else SynErr(253);
+		} else SynErr(254);
 	}
 
 	void AndOp() {
-		if (la.kind == 133) {
+		if (la.kind == 134) {
 			Get();
-		} else if (la.kind == 134) {
+		} else if (la.kind == 135) {
 			Get();
-		} else SynErr(254);
+		} else SynErr(255);
 	}
 
 	void OrOp() {
-		if (la.kind == 135) {
+		if (la.kind == 136) {
 			Get();
-		} else if (la.kind == 136) {
+		} else if (la.kind == 137) {
 			Get();
-		} else SynErr(255);
+		} else SynErr(256);
 	}
 
 	void NegOp() {
-		if (la.kind == 102) {
+		if (la.kind == 103) {
 			Get();
-		} else if (la.kind == 137) {
+		} else if (la.kind == 138) {
 			Get();
-		} else SynErr(256);
+		} else SynErr(257);
 	}
 
 	void Forall() {
-		if (la.kind == 119) {
+		if (la.kind == 120) {
 			Get();
-		} else if (la.kind == 138) {
+		} else if (la.kind == 139) {
 			Get();
-		} else SynErr(257);
+		} else SynErr(258);
 	}
 
 	void Exists() {
-		if (la.kind == 139) {
+		if (la.kind == 140) {
 			Get();
-		} else if (la.kind == 140) {
+		} else if (la.kind == 141) {
 			Get();
-		} else SynErr(258);
+		} else SynErr(259);
 	}
 
 	void QSep() {
@@ -4175,7 +4166,7 @@ void QSep() {
 			Get();
 		} else if (la.kind == 31) {
 			Get();
-		} else SynErr(259);
+		} else SynErr(260);
 	}
 
 	void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda, bool allowBitwiseOps) {
@@ -4193,12 +4184,12 @@ void ImpliesExpliesExpression(out Expression e0, bool allowSemi, bool allowLambd
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 
 		LogicalExpression(out e0, allowSemi, allowLambda, allowBitwiseOps);
 		if (IsImpliesOp() || IsExpliesOp()) {
-			if (la.kind == 129 || la.kind == 130) {
+			if (la.kind == 130 || la.kind == 131) {
 				ImpliesOp();
 				x = t; 
 				ImpliesExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
 				e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); 
-			} else if (la.kind == 131 || la.kind == 132) {
+			} else if (la.kind == 132 || la.kind == 133) {
 				ExpliesOp();
 				x = t; 
 				LogicalExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
@@ -4210,7 +4201,7 @@ void ImpliesExpliesExpression(out Expression e0, bool allowSemi, bool allowLambd
 					e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e1, e0);
 					
 				}
-			} else SynErr(260);
+			} else SynErr(261);
 		}
 	}
 
@@ -4219,7 +4210,7 @@ void LogicalExpression(out Expression e0, bool allowSemi, bool allowLambda, bool
 		Expression first;
 		e0 = dummyExpr; /* mute the warning */
 		
-		if (la.kind == 133 || la.kind == 134) {
+		if (la.kind == 134 || la.kind == 135) {
 			AndOp();
 			x = t; 
 			RelationalExpression(out e0, allowSemi, allowLambda, allowBitwiseOps);
@@ -4236,7 +4227,7 @@ void LogicalExpression(out Expression e0, bool allowSemi, bool allowLambda, bool
 			 e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, new LiteralExpr(x, true), e0);
 			}
 			
-		} else if (la.kind == 135 || la.kind == 136) {
+		} else if (la.kind == 136 || la.kind == 137) {
 			OrOp();
 			x = t; 
 			RelationalExpression(out e0, allowSemi, allowLambda, allowBitwiseOps);
@@ -4256,7 +4247,7 @@ void LogicalExpression(out Expression e0, bool allowSemi, bool allowLambda, bool
 		} else if (StartOf(31)) {
 			RelationalExpression(out e0, allowSemi, allowLambda, allowBitwiseOps);
 			if (IsAndOp() || IsOrOp()) {
-				if (la.kind == 133 || la.kind == 134) {
+				if (la.kind == 134 || la.kind == 135) {
 					AndOp();
 					x = t; 
 					RelationalExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
@@ -4267,7 +4258,7 @@ void LogicalExpression(out Expression e0, bool allowSemi, bool allowLambda, bool
 						RelationalExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
 						e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1); 
 					}
-				} else if (la.kind == 135 || la.kind == 136) {
+				} else if (la.kind == 136 || la.kind == 137) {
 					OrOp();
 					x = t; 
 					RelationalExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
@@ -4278,9 +4269,9 @@ void LogicalExpression(out Expression e0, bool allowSemi, bool allowLambda, bool
 						RelationalExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
 						e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1); 
 					}
-				} else SynErr(261);
+				} else SynErr(262);
 			}
-		} else SynErr(262);
+		} else SynErr(263);
 	}
 
 	void ImpliesExpression(out Expression e0, bool allowSemi, bool allowLambda, bool allowBitwiseOps) {
@@ -4390,17 +4381,17 @@ void ShiftTerm(out Expression e0, bool allowSemi, bool allowLambda, bool allowBi
 		
 		Term(out e0, allowSemi, allowLambda, allowBitwiseOps);
 		while (IsShiftOp()) {
-			if (la.kind == 80) {
+			if (la.kind == 81) {
 				Get();
 				x = t;  op = BinaryExpr.Opcode.LeftShift; 
-				Expect(80);
+				Expect(81);
 				x.val = "<<";  Contract.Assert(t.pos == x.pos + 1); 
-			} else if (la.kind == 81) {
+			} else if (la.kind == 82) {
 				Get();
 				x = t;  op = BinaryExpr.Opcode.RightShift; 
-				Expect(81);
+				Expect(82);
 				x.val = "<<";  Contract.Assert(t.pos == x.pos + 1); 
-			} else SynErr(263);
+			} else SynErr(264);
 			Term(out e1, allowSemi, allowLambda, allowBitwiseOps);
 			e0 = new BinaryExpr(x, op, e0, e1); 
 		}
@@ -4413,45 +4404,45 @@ void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k) {
 		k = null;
 		
 		switch (la.kind) {
-		case 82: {
+		case 83: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Eq; 
-			if (la.kind == 122) {
+			if (la.kind == 123) {
 				Get();
-				Expect(76);
-				Expression(out k, true, true);
 				Expect(77);
+				Expression(out k, true, true);
+				Expect(78);
 			}
 			break;
 		}
-		case 80: {
+		case 81: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Lt; 
 			break;
 		}
-		case 81: {
+		case 82: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Gt; 
 			break;
 		}
-		case 123: {
+		case 124: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 124: {
+		case 125: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		case 83: {
+		case 84: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
-			if (la.kind == 122) {
+			if (la.kind == 123) {
 				Get();
-				Expect(76);
-				Expression(out k, true, true);
 				Expect(77);
+				Expression(out k, true, true);
+				Expect(78);
 			}
 			break;
 		}
@@ -4460,16 +4451,16 @@ void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k) {
 			x = t;  op = BinaryExpr.Opcode.In; 
 			break;
 		}
-		case 86: {
+		case 87: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.NotIn; 
 			break;
 		}
-		case 102: {
+		case 103: {
 			Get();
 			x = t;  y = Token.NoToken; 
 			if (la.val == "!") {
-				Expect(102);
+				Expect(103);
 				y = t; 
 			}
 			if (y == Token.NoToken) {
@@ -4483,22 +4474,22 @@ void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op, out Expression k) {
 			
 			break;
 		}
-		case 84: {
+		case 85: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Neq; 
 			break;
 		}
-		case 125: {
+		case 126: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Le; 
 			break;
 		}
-		case 126: {
+		case 127: {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(264); break;
+		default: SynErr(265); break;
 		}
 	}
 
@@ -4524,27 +4515,27 @@ void Factor(out Expression e0, bool allowSemi, bool allowLambda, bool allowBitwi
 
 	void AddOp(out IToken x, out BinaryExpr.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op=BinaryExpr.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 101) {
+		if (la.kind == 102) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Add; 
-		} else if (la.kind == 103) {
+		} else if (la.kind == 104) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Sub; 
-		} else SynErr(265);
+		} else SynErr(266);
 	}
 
 	void BitvectorFactor(out Expression e0, bool allowSemi, bool allowLambda, bool allowBitwiseOps) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 
 		AsExpression(out e0, allowSemi, allowLambda, allowBitwiseOps);
 		if (allowBitwiseOps && IsBitwiseOp()) {
-			if (la.kind == 143) {
+			if (la.kind == 144) {
 				op = BinaryExpr.Opcode.BitwiseAnd; 
 				Get();
 				x = t; 
 				AsExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
 				e0 = new BinaryExpr(x, op, e0, e1); 
 				while (IsBitwiseAndOp()) {
-					Expect(143);
+					Expect(144);
 					x = t; 
 					AsExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
 					e0 = new BinaryExpr(x, op, e0, e1); 
@@ -4561,34 +4552,34 @@ void BitvectorFactor(out Expression e0, bool allowSemi, bool allowLambda, bool a
 					AsExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
 					e0 = new BinaryExpr(x, op, e0, e1); 
 				}
-			} else if (la.kind == 144) {
+			} else if (la.kind == 145) {
 				op = BinaryExpr.Opcode.BitwiseXor; 
 				Get();
 				x = t; 
 				AsExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
 				e0 = new BinaryExpr(x, op, e0, e1); 
 				while (IsBitwiseXorOp()) {
-					Expect(144);
+					Expect(145);
 					x = t; 
 					AsExpression(out e1, allowSemi, allowLambda, allowBitwiseOps);
 					e0 = new BinaryExpr(x, op, e0, e1); 
 				}
-			} else SynErr(266);
+			} else SynErr(267);
 		}
 	}
 
 	void MulOp(out IToken x, out BinaryExpr.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken;  op = BinaryExpr.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 85) {
+		if (la.kind == 86) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mul; 
-		} else if (la.kind == 141) {
+		} else if (la.kind == 142) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Div; 
-		} else if (la.kind == 142) {
+		} else if (la.kind == 143) {
 			Get();
 			x = t;  op = BinaryExpr.Opcode.Mod; 
-		} else SynErr(267);
+		} else SynErr(268);
 	}
 
 	void AsExpression(out Expression e, bool allowSemi, bool allowLambda, bool allowBitwiseOps) {
@@ -4604,12 +4595,12 @@ void AsExpression(out Expression e, bool allowSemi, bool allowLambda, bool allow
 
 	void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda, bool allowBitwiseOps) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 
-		if (la.kind == 103) {
+		if (la.kind == 104) {
 			Get();
 			x = t; 
 			UnaryExpression(out e, allowSemi, allowLambda, allowBitwiseOps);
 			e = new NegationExpression(x, e); 
-		} else if (la.kind == 102 || la.kind == 137) {
+		} else if (la.kind == 103 || la.kind == 138) {
 			NegOp();
 			x = t; 
 			UnaryExpression(out e, allowSemi, allowLambda, allowBitwiseOps);
@@ -4644,7 +4635,7 @@ void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda, bool al
 			while (IsSuffix()) {
 				Suffix(ref e);
 			}
-		} else if (la.kind == 74 || la.kind == 76) {
+		} else if (la.kind == 75 || la.kind == 77) {
 			DisplayExpr(out e);
 			while (IsSuffix()) {
 				Suffix(ref e);
@@ -4664,7 +4655,7 @@ void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda, bool al
 			while (IsSuffix()) {
 				Suffix(ref e);
 			}
-		} else SynErr(268);
+		} else SynErr(269);
 	}
 
 	void MapDisplayExpr(IToken/*!*/ mapToken, bool finite, out Expression e) {
@@ -4672,12 +4663,12 @@ void MapDisplayExpr(IToken/*!*/ mapToken, bool finite, out Expression e) {
 		List<ExpressionPair/*!*/>/*!*/ elements= new List<ExpressionPair/*!*/>() ;
 		e = dummyExpr;
 		
-		Expect(76);
+		Expect(77);
 		if (StartOf(8)) {
 			MapLiteralExpressions(out elements);
 		}
 		e = new MapDisplayExpr(mapToken, finite, elements);
-		Expect(77);
+		Expect(78);
 	}
 
 	void Suffix(ref Expression e) {
@@ -4691,7 +4682,7 @@ void Suffix(ref Expression e) {
 		
 		if (la.kind == 32) {
 			Get();
-			if (la.kind == 78) {
+			if (la.kind == 79) {
 				Get();
 				x = t; updates = new List<Tuple<IToken, string, Expression>>(); 
 				MemberBindingUpdate(out id, out v);
@@ -4701,7 +4692,7 @@ void Suffix(ref Expression e) {
 					MemberBindingUpdate(out id, out v);
 					updates.Add(Tuple.Create(id, id.val, v)); 
 				}
-				Expect(79);
+				Expect(80);
 				e = new DatatypeUpdateExpr(x, e, updates); 
 			} else if (StartOf(33)) {
 				DotSuffix(out id, out x);
@@ -4715,23 +4706,23 @@ void Suffix(ref Expression e) {
 				if (IsGenericInstantiation(true)) {
 					typeArgs = new List<Type>(); 
 					GenericInstantiation(typeArgs);
-				} else if (la.kind == 122) {
+				} else if (la.kind == 123) {
 					HashCall(id, out openParen, out typeArgs, out args);
 				} else if (StartOf(34)) {
-				} else SynErr(269);
+				} else SynErr(270);
 				e = new ExprDotName(id, e, id.val, typeArgs);
 				if (openParen != null) {
 				 e = new ApplySuffix(openParen, e, args);
 				}
 				
-			} else SynErr(270);
-		} else if (la.kind == 76) {
+			} else SynErr(271);
+		} else if (la.kind == 77) {
 			Get();
 			x = t; 
 			if (StartOf(8)) {
 				Expression(out ee, true, true);
 				e0 = ee; 
-				if (la.kind == 154) {
+				if (la.kind == 155) {
 					Get();
 					anyDots = true; 
 					if (StartOf(8)) {
@@ -4761,7 +4752,7 @@ void Suffix(ref Expression e) {
 							takeRest = true; 
 						}
 					}
-				} else if (la.kind == 26 || la.kind == 77) {
+				} else if (la.kind == 26 || la.kind == 78) {
 					while (la.kind == 26) {
 						Get();
 						Expression(out ee, true, true);
@@ -4772,15 +4763,15 @@ void Suffix(ref Expression e) {
 						multipleIndices.Add(ee);
 						
 					}
-				} else SynErr(271);
-			} else if (la.kind == 154) {
+				} else SynErr(272);
+			} else if (la.kind == 155) {
 				Get();
 				anyDots = true; 
 				if (StartOf(8)) {
 					Expression(out ee, true, true);
 					e1 = ee; 
 				}
-			} else SynErr(272);
+			} else SynErr(273);
 			if (multipleIndices != null) {
 			 e = new MultiSelectExpr(x, e, multipleIndices);
 			 // make sure an array class with this dimensionality exists
@@ -4815,16 +4806,16 @@ void Suffix(ref Expression e) {
 			 }
 			}
 			
-			Expect(77);
-		} else if (la.kind == 78) {
+			Expect(78);
+		} else if (la.kind == 79) {
 			Get();
 			IToken openParen = t; var args = new List<Expression>(); 
 			if (StartOf(8)) {
 				Expressions(args);
 			}
-			Expect(79);
+			Expect(80);
 			e = new ApplySuffix(openParen, e, args); 
-		} else SynErr(273);
+		} else SynErr(274);
 	}
 
 	void ISetDisplayExpr(IToken/*!*/ setToken, bool finite, out Expression e) {
@@ -4832,12 +4823,12 @@ void ISetDisplayExpr(IToken/*!*/ setToken, bool finite, out Expression e) {
 		List<Expression> elements = new List<Expression/*!*/>();;
 		e = dummyExpr;
 		
-		Expect(74);
+		Expect(75);
 		if (StartOf(8)) {
 			Expressions(elements);
 		}
 		e = new SetDisplayExpr(setToken, finite, elements);
-		Expect(75);
+		Expect(76);
 	}
 
 	void LambdaExpression(out Expression e, bool allowSemi, bool allowBitwiseOps) {
@@ -4852,7 +4843,7 @@ void LambdaExpression(out Expression e, bool allowSemi, bool allowBitwiseOps) {
 		if (la.kind == 1) {
 			WildIdent(out id, true);
 			x = t; bvs.Add(new BoundVar(id, id.val, new InferredTypeProxy())); 
-		} else if (la.kind == 78) {
+		} else if (la.kind == 79) {
 			Get();
 			x = t; 
 			if (la.kind == 1) {
@@ -4864,8 +4855,8 @@ void LambdaExpression(out Expression e, bool allowSemi, bool allowBitwiseOps) {
 					bvs.Add(bv); 
 				}
 			}
-			Expect(79);
-		} else SynErr(274);
+			Expect(80);
+		} else SynErr(275);
 		while (la.kind == 69 || la.kind == 70) {
 			if (la.kind == 69) {
 				Get();
@@ -4897,7 +4888,7 @@ void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda, bool
 		e = dummyExpr;
 		
 		switch (la.kind) {
-		case 114: {
+		case 115: {
 			Get();
 			x = t; 
 			if (IsExistentialGuard()) {
@@ -4905,7 +4896,7 @@ void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda, bool
 				isExistentialGuard = true; 
 			} else if (StartOf(8)) {
 				Expression(out e, true, true);
-			} else SynErr(275);
+			} else SynErr(276);
 			Expect(39);
 			Expression(out e0, true, true, true);
 			Expect(40);
@@ -4922,11 +4913,11 @@ void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda, bool
 			
 			break;
 		}
-		case 116: {
+		case 117: {
 			MatchExpression(out e, allowSemi, allowLambda, allowBitwiseOps);
 			break;
 		}
-		case 119: case 138: case 139: case 140: {
+		case 120: case 139: case 140: case 141: {
 			QuantifierGuts(out e, allowSemi, allowLambda);
 			break;
 		}
@@ -4942,7 +4933,7 @@ void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda, bool
 			SetComprehensionExpr(x, false, out e, allowSemi, allowLambda, true);
 			break;
 		}
-		case 36: case 37: case 117: {
+		case 36: case 37: case 118: {
 			StmtInExpr(out s);
 			Expression(out e, allowSemi, allowLambda, allowBitwiseOps);
 			e = new StmtExpr(s.Tok, s, e); 
@@ -4964,17 +4955,17 @@ void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda, bool
 			MapComprehensionExpr(x, false, out e, allowSemi, allowLambda, true);
 			break;
 		}
-		case 88: {
+		case 89: {
 			Get();
 			Expression(out e, false, false, allowBitwiseOps);
 			e = new RevealExpr(e.tok, e); 
 			break;
 		}
-		case 110: {
+		case 111: {
 			NamedExpr(out e, allowSemi, allowLambda, allowBitwiseOps);
 			break;
 		}
-		default: SynErr(276); break;
+		default: SynErr(277); break;
 		}
 	}
 
@@ -4986,10 +4977,10 @@ void NameSegment(out Expression e) {
 		if (IsGenericInstantiation(true)) {
 			typeArgs = new List<Type>(); 
 			GenericInstantiation(typeArgs);
-		} else if (la.kind == 122) {
+		} else if (la.kind == 123) {
 			HashCall(id, out openParen, out typeArgs, out args);
 		} else if (StartOf(34)) {
-		} else SynErr(277);
+		} else SynErr(278);
 		e = new NameSegment(id, id.val, typeArgs);
 		if (openParen != null) {
 		 e = new ApplySuffix(openParen, e, args);
@@ -5002,23 +4993,23 @@ void DisplayExpr(out Expression e) {
 		IToken x;  List<Expression> elements;
 		e = dummyExpr;
 		
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			Get();
 			x = t;  elements = new List<Expression/*!*/>(); 
 			if (StartOf(8)) {
 				Expressions(elements);
 			}
 			e = new SetDisplayExpr(x, true, elements);
-			Expect(75);
-		} else if (la.kind == 76) {
+			Expect(76);
+		} else if (la.kind == 77) {
 			Get();
 			x = t;  elements = new List<Expression/*!*/>(); 
 			if (StartOf(8)) {
 				Expressions(elements);
 			}
 			e = new SeqDisplayExpr(x, elements); 
-			Expect(77);
-		} else SynErr(278);
+			Expect(78);
+		} else SynErr(279);
 	}
 
 	void MultiSetExpr(out Expression e) {
@@ -5028,21 +5019,21 @@ void MultiSetExpr(out Expression e) {
 		
 		Expect(19);
 		x = t; 
-		if (la.kind == 74) {
+		if (la.kind == 75) {
 			Get();
 			elements = new List<Expression/*!*/>(); 
 			if (StartOf(8)) {
 				Expressions(elements);
 			}
 			e = new MultiSetDisplayExpr(x, elements);
-			Expect(75);
-		} else if (la.kind == 78) {
+			Expect(76);
+		} else if (la.kind == 79) {
 			Get();
 			x = t;  elements = new List<Expression/*!*/>(); 
 			Expression(out e, true, true);
 			e = new MultiSetFormingExpr(x, e); 
-			Expect(79);
-		} else SynErr(279);
+			Expect(80);
+		} else SynErr(280);
 	}
 
 	void SeqConstructionExpr(out Expression e) {
@@ -5053,11 +5044,11 @@ void SeqConstructionExpr(out Expression e) {
 		
 		Expect(20);
 		x = t; 
-		Expect(78);
+		Expect(79);
 		Expression(out n, true, true);
 		Expect(26);
 		Expression(out f, true, true);
-		Expect(79);
+		Expect(80);
 		e = new SeqConstructionExpr(x, n, f); 
 	}
 
@@ -5067,17 +5058,17 @@ void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) {
 		e = dummyExpr;  Type toType = null;
 		
 		switch (la.kind) {
-		case 145: {
+		case 146: {
 			Get();
 			e = new LiteralExpr(t, false); 
 			break;
 		}
-		case 146: {
+		case 147: {
 			Get();
 			e = new LiteralExpr(t, true); 
 			break;
 		}
-		case 147: {
+		case 148: {
 			Get();
 			e = new LiteralExpr(t); 
 			break;
@@ -5105,37 +5096,37 @@ void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) {
 			
 			break;
 		}
-		case 148: {
+		case 149: {
 			Get();
 			e = new ThisExpr(t); 
 			break;
 		}
-		case 149: {
+		case 150: {
 			Get();
 			x = t; 
-			Expect(78);
-			Expression(out e, true, true);
 			Expect(79);
+			Expression(out e, true, true);
+			Expect(80);
 			e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Fresh, e); 
 			break;
 		}
-		case 150: {
+		case 151: {
 			Get();
 			x = t; 
-			Expect(78);
-			Expression(out e, true, true);
 			Expect(79);
+			Expression(out e, true, true);
+			Expect(80);
 			e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Allocated, e); 
 			break;
 		}
-		case 151: {
+		case 152: {
 			Get();
 			x = t; FrameExpression fe; var mod = new List<FrameExpression>(); IToken oldAt = null; 
-			if (la.kind == 152) {
+			if (la.kind == 153) {
 				Get();
 				LabelIdent(out oldAt);
 			}
-			Expect(78);
+			Expect(79);
 			FrameExpression(out fe, false, false);
 			mod.Add(fe); 
 			while (la.kind == 26) {
@@ -5143,20 +5134,20 @@ void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) {
 				FrameExpression(out fe, false, false);
 				mod.Add(fe); 
 			}
-			Expect(79);
+			Expect(80);
 			e = new UnchangedExpr(x, mod, oldAt?.val); 
 			break;
 		}
-		case 153: {
+		case 154: {
 			Get();
 			x = t; IToken oldAt = null; 
-			if (la.kind == 152) {
+			if (la.kind == 153) {
 				Get();
 				LabelIdent(out oldAt);
 			}
-			Expect(78);
-			Expression(out e, true, true);
 			Expect(79);
+			Expression(out e, true, true);
+			Expect(80);
 			e = new OldExpr(x, e, oldAt?.val); 
 			break;
 		}
@@ -5177,17 +5168,17 @@ void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) {
 				x = t; toType = new RealType(); 
 			}
 			errors.Deprecated(t, string.Format("the syntax \"{0}(expr)\" for type conversions has been deprecated; the new syntax is \"expr as {0}\"", x.val)); 
-			Expect(78);
-			Expression(out e, true, true);
 			Expect(79);
+			Expression(out e, true, true);
+			Expect(80);
 			e = new ConversionExpr(x, e, toType); 
 			break;
 		}
-		case 78: {
+		case 79: {
 			ParensExpression(out e, allowSemi, allowLambda);
 			break;
 		}
-		default: SynErr(280); break;
+		default: SynErr(281); break;
 		}
 	}
 
@@ -5216,7 +5207,7 @@ void Nat(out BigInteger n) {
 			 n = BigInteger.Zero;
 			}
 			
-		} else SynErr(281);
+		} else SynErr(282);
 	}
 
 	void Dec(out Basetypes.BigDec d) {
@@ -5236,12 +5227,12 @@ void ParensExpression(out Expression e, bool allowSemi, bool allowLambda) {
 		IToken x;
 		var args = new List<Expression>();
 		
-		Expect(78);
+		Expect(79);
 		x = t; 
 		if (StartOf(8)) {
 			Expressions(args);
 		}
-		Expect(79);
+		Expect(80);
 		if (args.Count == 1) {
 		 e = new ParensExpression(x, args[0]);
 		} else {
@@ -5316,23 +5307,23 @@ void MatchExpression(out Expression e, bool allowSemi, bool allowLambda, bool al
 		List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
 		bool usesOptionalBraces = false;
 		
-		Expect(116);
+		Expect(117);
 		x = t; 
 		Expression(out e, allowSemi, allowLambda, allowBitwiseOps);
 		if (la.kind == _lbrace) {
-			Expect(74);
+			Expect(75);
 			usesOptionalBraces = true; 
 			while (la.kind == 38) {
 				CaseExpression(out c, true, true, allowBitwiseOps);
 				cases.Add(c); 
 			}
-			Expect(75);
+			Expect(76);
 		} else if (StartOf(35)) {
 			while (la.kind == _case) {
 				CaseExpression(out c, allowSemi, allowLambda, allowBitwiseOps);
 				cases.Add(c); 
 			}
-		} else SynErr(282);
+		} else SynErr(283);
 		e = new MatchExpr(x, e, cases, usesOptionalBraces); 
 	}
 
@@ -5344,13 +5335,13 @@ void QuantifierGuts(out Expression q, bool allowSemi, bool allowLambda) {
 		Expression range;
 		Expression/*!*/ body;
 		
-		if (la.kind == 119 || la.kind == 138) {
+		if (la.kind == 120 || la.kind == 139) {
 			Forall();
 			x = t;  univ = true; 
-		} else if (la.kind == 139 || la.kind == 140) {
+		} else if (la.kind == 140 || la.kind == 141) {
 			Exists();
 			x = t; 
-		} else SynErr(283);
+		} else SynErr(284);
 		QuantifierDomain(out bvars, out attrs, out range);
 		QSep();
 		Expression(out body, allowSemi, allowLambda);
@@ -5397,13 +5388,13 @@ void SetComprehensionExpr(IToken setToken, bool finite, out Expression q, bool a
 
 	void StmtInExpr(out Statement s) {
 		s = dummyStmt; 
-		if (la.kind == 117) {
+		if (la.kind == 118) {
 			AssertStmt(out s, true);
 		} else if (la.kind == 36) {
 			AssumeStmt(out s);
 		} else if (la.kind == 37) {
 			CalcStmt(out s);
-		} else SynErr(284);
+		} else SynErr(285);
 	}
 
 	void LetExpr(out Expression e, bool allowSemi, bool allowLambda, bool allowBitwiseOps) {
@@ -5447,7 +5438,7 @@ void LetExpr(out Expression e, bool allowSemi, bool allowLambda, bool allowBitwi
 			 }
 			}
 			
-		} else SynErr(285);
+		} else SynErr(286);
 		Expression(out e, false, true);
 		letRHSs.Add(e); 
 		while (la.kind == 26) {
@@ -5465,7 +5456,7 @@ void NamedExpr(out Expression e, bool allowSemi, bool allowLambda, bool allowBit
 		e = dummyExpr;
 		Expression expr;
 		
-		Expect(110);
+		Expect(111);
 		x = t; 
 		NoUSIdent(out d);
 		Expect(25);
@@ -5486,9 +5477,9 @@ void CaseExpression(out MatchCaseExpr c, bool allowSemi, bool allowLambda, bool
 		if (la.kind == 1) {
 			Ident(out id);
 			name = id.val; 
-			if (la.kind == 78) {
+			if (la.kind == 79) {
 				Get();
-				if (la.kind == 1 || la.kind == 78) {
+				if (la.kind == 1 || la.kind == 79) {
 					CasePattern(out pat);
 					arguments.Add(pat); 
 					while (la.kind == 26) {
@@ -5497,9 +5488,9 @@ void CaseExpression(out MatchCaseExpr c, bool allowSemi, bool allowLambda, bool
 						arguments.Add(pat); 
 					}
 				}
-				Expect(79);
+				Expect(80);
 			}
-		} else if (la.kind == 78) {
+		} else if (la.kind == 79) {
 			Get();
 			CasePattern(out pat);
 			arguments.Add(pat); 
@@ -5508,8 +5499,8 @@ void CaseExpression(out MatchCaseExpr c, bool allowSemi, bool allowLambda, bool
 				CasePattern(out pat);
 				arguments.Add(pat); 
 			}
-			Expect(79);
-		} else SynErr(286);
+			Expect(80);
+		} else SynErr(287);
 		Expect(35);
 		Expression(out body, allowSemi, allowLambda, allowBitwiseOps);
 		c = new MatchCaseExpr(x, name, arguments, body); 
@@ -5517,22 +5508,22 @@ void CaseExpression(out MatchCaseExpr c, bool allowSemi, bool allowLambda, bool
 
 	void HashCall(IToken id, out IToken openParen, out List<Type> typeArgs, out List<Expression> args) {
 		Expression k; args = new List<Expression>(); typeArgs = null; 
-		Expect(122);
+		Expect(123);
 		id.val = id.val + "#"; 
-		if (la.kind == 80) {
+		if (la.kind == 81) {
 			typeArgs = new List<Type>(); 
 			GenericInstantiation(typeArgs);
 		}
-		Expect(76);
-		Expression(out k, true, true);
 		Expect(77);
-		args.Add(k); 
+		Expression(out k, true, true);
 		Expect(78);
+		args.Add(k); 
+		Expect(79);
 		openParen = t; 
 		if (StartOf(8)) {
 			Expressions(args);
 		}
-		Expect(79);
+		Expect(80);
 	}
 
 	void MemberBindingUpdate(out IToken id, out Expression e) {
@@ -5543,7 +5534,7 @@ void MemberBindingUpdate(out IToken id, out Expression e) {
 		} else if (la.kind == 2) {
 			Get();
 			id = t; 
-		} else SynErr(287);
+		} else SynErr(288);
 		Expect(29);
 		Expression(out e, true, true);
 	}
@@ -5586,7 +5577,7 @@ void DotSuffix(out IToken x, out IToken y) {
 		} else if (la.kind == 69) {
 			Get();
 			x = t; 
-		} else SynErr(288);
+		} else SynErr(289);
 	}
 
 
@@ -5601,42 +5592,42 @@ public void Parse() {
   }
 
   static readonly bool[,] set = {
-		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_x, _T,_T,_T,_x, _x,_x,_x,_x, _T,_T,_x,_x, _T,_T,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_T, _T,_x,_T,_T, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_T,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_T,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_T,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_T,_T, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_T,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _x,_T,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_x, _x,_x,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_x, _x},
-		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_T,_T,_T, _T,_T,_T,_x, _x,_x,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_x, _x}
+		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_x, _T,_T,_T,_x, _x,_x,_x,_x, _T,_T,_x,_x, _T,_T,_x,_T, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_x, _T,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_T,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_T, _T,_x,_x,_T, _T,_x,_x,_T, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_T,_T,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_T,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_T,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_T,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_x,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_T,_T,_T, _T,_T,_T,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_T, _x,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_x,_T,_x, _x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_T, _x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x},
+		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _x,_x},
+		{_T,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_x,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_x,_x,_x, _x,_x,_x,_T, _x,_x,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_x,_T,_T, _x,_x}
 
   };
 } // end Parser
@@ -5738,221 +5729,222 @@ string GetSyntaxErrorString(int n) {
 			case 71: s = "ensures expected"; break;
 			case 72: s = "ghost expected"; break;
 			case 73: s = "witness expected"; break;
-			case 74: s = "lbrace expected"; break;
-			case 75: s = "rbrace expected"; break;
-			case 76: s = "lbracket expected"; break;
-			case 77: s = "rbracket expected"; break;
-			case 78: s = "openparen expected"; break;
-			case 79: s = "closeparen expected"; break;
-			case 80: s = "openAngleBracket expected"; break;
-			case 81: s = "closeAngleBracket expected"; break;
-			case 82: s = "eq expected"; break;
-			case 83: s = "neq expected"; break;
-			case 84: s = "neqAlt expected"; break;
-			case 85: s = "star expected"; break;
-			case 86: s = "notIn expected"; break;
-			case 87: s = "ellipsis expected"; break;
-			case 88: s = "reveal expected"; break;
-			case 89: s = "\"include\" expected"; break;
-			case 90: s = "\"abstract\" expected"; break;
-			case 91: s = "\"module\" expected"; break;
-			case 92: s = "\"refines\" expected"; break;
-			case 93: s = "\"opened\" expected"; break;
-			case 94: s = "\"=\" expected"; break;
-			case 95: s = "\"provides\" expected"; break;
-			case 96: s = "\"reveals\" expected"; break;
-			case 97: s = "\"extends\" expected"; break;
-			case 98: s = "\"new\" expected"; break;
-			case 99: s = "\"yields\" expected"; break;
-			case 100: s = "\"returns\" expected"; break;
-			case 101: s = "\"+\" expected"; break;
-			case 102: s = "\"!\" expected"; break;
-			case 103: s = "\"-\" expected"; break;
-			case 104: s = "\"comethod\" expected"; break;
-			case 105: s = "\"free\" expected"; break;
-			case 106: s = "\"yield\" expected"; break;
-			case 107: s = "\"~>\" expected"; break;
-			case 108: s = "\"-->\" expected"; break;
-			case 109: s = "\"->\" expected"; break;
-			case 110: s = "\"label\" expected"; break;
-			case 111: s = "\"break\" expected"; break;
-			case 112: s = "\"where\" expected"; break;
-			case 113: s = "\"return\" expected"; break;
-			case 114: s = "\"if\" expected"; break;
-			case 115: s = "\"while\" expected"; break;
-			case 116: s = "\"match\" expected"; break;
-			case 117: s = "\"assert\" expected"; break;
-			case 118: s = "\"print\" expected"; break;
-			case 119: s = "\"forall\" expected"; break;
-			case 120: s = "\"parallel\" expected"; break;
-			case 121: s = "\"modify\" expected"; break;
-			case 122: s = "\"#\" expected"; break;
-			case 123: s = "\"<=\" expected"; break;
-			case 124: s = "\">=\" expected"; break;
-			case 125: s = "\"\\u2264\" expected"; break;
-			case 126: s = "\"\\u2265\" expected"; break;
-			case 127: s = "\"<==>\" expected"; break;
-			case 128: s = "\"\\u21d4\" expected"; break;
-			case 129: s = "\"==>\" expected"; break;
-			case 130: s = "\"\\u21d2\" expected"; break;
-			case 131: s = "\"<==\" expected"; break;
-			case 132: s = "\"\\u21d0\" expected"; break;
-			case 133: s = "\"&&\" expected"; break;
-			case 134: s = "\"\\u2227\" expected"; break;
-			case 135: s = "\"||\" expected"; break;
-			case 136: s = "\"\\u2228\" expected"; break;
-			case 137: s = "\"\\u00ac\" expected"; break;
-			case 138: s = "\"\\u2200\" expected"; break;
-			case 139: s = "\"exists\" expected"; break;
-			case 140: s = "\"\\u2203\" expected"; break;
-			case 141: s = "\"/\" expected"; break;
-			case 142: s = "\"%\" expected"; break;
-			case 143: s = "\"&\" expected"; break;
-			case 144: s = "\"^\" expected"; break;
-			case 145: s = "\"false\" expected"; break;
-			case 146: s = "\"true\" expected"; break;
-			case 147: s = "\"null\" expected"; break;
-			case 148: s = "\"this\" expected"; break;
-			case 149: s = "\"fresh\" expected"; break;
-			case 150: s = "\"allocated\" expected"; break;
-			case 151: s = "\"unchanged\" expected"; break;
-			case 152: s = "\"@\" expected"; break;
-			case 153: s = "\"old\" expected"; break;
-			case 154: s = "\"..\" expected"; break;
-			case 155: s = "??? expected"; break;
-			case 156: s = "invalid TopDecl"; break;
-			case 157: s = "invalid DeclModifier"; break;
-			case 158: s = "invalid SubModuleDecl"; break;
-			case 159: s = "this symbol not expected in SubModuleDecl"; break;
-			case 160: s = "invalid SubModuleDecl"; break;
+			case 74: s = "lbracecolon expected"; break;
+			case 75: s = "lbrace expected"; break;
+			case 76: s = "rbrace expected"; break;
+			case 77: s = "lbracket expected"; break;
+			case 78: s = "rbracket expected"; break;
+			case 79: s = "openparen expected"; break;
+			case 80: s = "closeparen expected"; break;
+			case 81: s = "openAngleBracket expected"; break;
+			case 82: s = "closeAngleBracket expected"; break;
+			case 83: s = "eq expected"; break;
+			case 84: s = "neq expected"; break;
+			case 85: s = "neqAlt expected"; break;
+			case 86: s = "star expected"; break;
+			case 87: s = "notIn expected"; break;
+			case 88: s = "ellipsis expected"; break;
+			case 89: s = "reveal expected"; break;
+			case 90: s = "\"include\" expected"; break;
+			case 91: s = "\"abstract\" expected"; break;
+			case 92: s = "\"module\" expected"; break;
+			case 93: s = "\"refines\" expected"; break;
+			case 94: s = "\"opened\" expected"; break;
+			case 95: s = "\"=\" expected"; break;
+			case 96: s = "\"provides\" expected"; break;
+			case 97: s = "\"reveals\" expected"; break;
+			case 98: s = "\"extends\" expected"; break;
+			case 99: s = "\"new\" expected"; break;
+			case 100: s = "\"yields\" expected"; break;
+			case 101: s = "\"returns\" expected"; break;
+			case 102: s = "\"+\" expected"; break;
+			case 103: s = "\"!\" expected"; break;
+			case 104: s = "\"-\" expected"; break;
+			case 105: s = "\"comethod\" expected"; break;
+			case 106: s = "\"free\" expected"; break;
+			case 107: s = "\"yield\" expected"; break;
+			case 108: s = "\"~>\" expected"; break;
+			case 109: s = "\"-->\" expected"; break;
+			case 110: s = "\"->\" expected"; break;
+			case 111: s = "\"label\" expected"; break;
+			case 112: s = "\"break\" expected"; break;
+			case 113: s = "\"where\" expected"; break;
+			case 114: s = "\"return\" expected"; break;
+			case 115: s = "\"if\" expected"; break;
+			case 116: s = "\"while\" expected"; break;
+			case 117: s = "\"match\" expected"; break;
+			case 118: s = "\"assert\" expected"; break;
+			case 119: s = "\"print\" expected"; break;
+			case 120: s = "\"forall\" expected"; break;
+			case 121: s = "\"parallel\" expected"; break;
+			case 122: s = "\"modify\" expected"; break;
+			case 123: s = "\"#\" expected"; break;
+			case 124: s = "\"<=\" expected"; break;
+			case 125: s = "\">=\" expected"; break;
+			case 126: s = "\"\\u2264\" expected"; break;
+			case 127: s = "\"\\u2265\" expected"; break;
+			case 128: s = "\"<==>\" expected"; break;
+			case 129: s = "\"\\u21d4\" expected"; break;
+			case 130: s = "\"==>\" expected"; break;
+			case 131: s = "\"\\u21d2\" expected"; break;
+			case 132: s = "\"<==\" expected"; break;
+			case 133: s = "\"\\u21d0\" expected"; break;
+			case 134: s = "\"&&\" expected"; break;
+			case 135: s = "\"\\u2227\" expected"; break;
+			case 136: s = "\"||\" expected"; break;
+			case 137: s = "\"\\u2228\" expected"; break;
+			case 138: s = "\"\\u00ac\" expected"; break;
+			case 139: s = "\"\\u2200\" expected"; break;
+			case 140: s = "\"exists\" expected"; break;
+			case 141: s = "\"\\u2203\" expected"; break;
+			case 142: s = "\"/\" expected"; break;
+			case 143: s = "\"%\" expected"; break;
+			case 144: s = "\"&\" expected"; break;
+			case 145: s = "\"^\" expected"; break;
+			case 146: s = "\"false\" expected"; break;
+			case 147: s = "\"true\" expected"; break;
+			case 148: s = "\"null\" expected"; break;
+			case 149: s = "\"this\" expected"; break;
+			case 150: s = "\"fresh\" expected"; break;
+			case 151: s = "\"allocated\" expected"; break;
+			case 152: s = "\"unchanged\" expected"; break;
+			case 153: s = "\"@\" expected"; break;
+			case 154: s = "\"old\" expected"; break;
+			case 155: s = "\"..\" expected"; break;
+			case 156: s = "??? expected"; break;
+			case 157: s = "invalid TopDecl"; break;
+			case 158: s = "invalid DeclModifier"; break;
+			case 159: s = "invalid SubModuleDecl"; break;
+			case 160: s = "this symbol not expected in SubModuleDecl"; break;
 			case 161: s = "invalid SubModuleDecl"; break;
 			case 162: s = "invalid SubModuleDecl"; break;
-			case 163: s = "this symbol not expected in ClassDecl"; break;
-			case 164: s = "this symbol not expected in DatatypeDecl"; break;
-			case 165: s = "invalid DatatypeDecl"; break;
-			case 166: s = "invalid NewtypeDecl"; break;
-			case 167: s = "invalid OtherTypeDecl"; break;
-			case 168: s = "this symbol not expected in OtherTypeDecl"; break;
-			case 169: s = "this symbol not expected in IteratorDecl"; break;
-			case 170: s = "invalid IteratorDecl"; break;
-			case 171: s = "this symbol not expected in TraitDecl"; break;
-			case 172: s = "invalid ClassMemberDecl"; break;
-			case 173: s = "invalid QualifiedModuleExportSuffix"; break;
+			case 163: s = "invalid SubModuleDecl"; break;
+			case 164: s = "this symbol not expected in ClassDecl"; break;
+			case 165: s = "this symbol not expected in DatatypeDecl"; break;
+			case 166: s = "invalid DatatypeDecl"; break;
+			case 167: s = "invalid NewtypeDecl"; break;
+			case 168: s = "invalid OtherTypeDecl"; break;
+			case 169: s = "this symbol not expected in OtherTypeDecl"; break;
+			case 170: s = "this symbol not expected in IteratorDecl"; break;
+			case 171: s = "invalid IteratorDecl"; break;
+			case 172: s = "this symbol not expected in TraitDecl"; break;
+			case 173: s = "invalid ClassMemberDecl"; break;
 			case 174: s = "invalid QualifiedModuleExportSuffix"; break;
-			case 175: s = "invalid TypeNameOrCtorSuffix"; break;
-			case 176: s = "this symbol not expected in FieldDecl"; break;
-			case 177: s = "this symbol not expected in ConstantFieldDecl"; break;
-			case 178: s = "invalid FunctionDecl"; break;
+			case 175: s = "invalid QualifiedModuleExportSuffix"; break;
+			case 176: s = "invalid TypeNameOrCtorSuffix"; break;
+			case 177: s = "this symbol not expected in FieldDecl"; break;
+			case 178: s = "this symbol not expected in ConstantFieldDecl"; break;
 			case 179: s = "invalid FunctionDecl"; break;
 			case 180: s = "invalid FunctionDecl"; break;
 			case 181: s = "invalid FunctionDecl"; break;
 			case 182: s = "invalid FunctionDecl"; break;
 			case 183: s = "invalid FunctionDecl"; break;
-			case 184: s = "this symbol not expected in MethodDecl"; break;
-			case 185: s = "invalid MethodDecl"; break;
+			case 184: s = "invalid FunctionDecl"; break;
+			case 185: s = "this symbol not expected in MethodDecl"; break;
 			case 186: s = "invalid MethodDecl"; break;
-			case 187: s = "invalid FIdentType"; break;
-			case 188: s = "this symbol not expected in OldSemi"; break;
-			case 189: s = "invalid CIdentType"; break;
-			case 190: s = "invalid TypeIdentOptional"; break;
-			case 191: s = "invalid TypeAndToken"; break;
-			case 192: s = "this symbol not expected in IteratorSpec"; break;
-			case 193: s = "invalid IteratorSpec"; break;
+			case 187: s = "invalid MethodDecl"; break;
+			case 188: s = "invalid FIdentType"; break;
+			case 189: s = "this symbol not expected in OldSemi"; break;
+			case 190: s = "invalid CIdentType"; break;
+			case 191: s = "invalid TypeIdentOptional"; break;
+			case 192: s = "invalid TypeAndToken"; break;
+			case 193: s = "this symbol not expected in IteratorSpec"; break;
 			case 194: s = "invalid IteratorSpec"; break;
-			case 195: s = "invalid Variance"; break;
-			case 196: s = "invalid TPCharOption"; break;
-			case 197: s = "invalid FuMe_Ident"; break;
-			case 198: s = "invalid KType"; break;
-			case 199: s = "this symbol not expected in MethodSpec"; break;
-			case 200: s = "invalid MethodSpec"; break;
+			case 195: s = "invalid IteratorSpec"; break;
+			case 196: s = "invalid Variance"; break;
+			case 197: s = "invalid TPCharOption"; break;
+			case 198: s = "invalid FuMe_Ident"; break;
+			case 199: s = "invalid KType"; break;
+			case 200: s = "this symbol not expected in MethodSpec"; break;
 			case 201: s = "invalid MethodSpec"; break;
-			case 202: s = "invalid FrameExpression"; break;
-			case 203: s = "invalid LabelIdent"; break;
-			case 204: s = "this symbol not expected in FunctionSpec"; break;
-			case 205: s = "invalid FunctionSpec"; break;
-			case 206: s = "invalid PossiblyWildFrameExpression"; break;
-			case 207: s = "invalid PossiblyWildExpression"; break;
-			case 208: s = "this symbol not expected in OneStmt"; break;
-			case 209: s = "invalid OneStmt"; break;
-			case 210: s = "this symbol not expected in OneStmt"; break;
-			case 211: s = "invalid OneStmt"; break;
-			case 212: s = "invalid AssertStmt"; break;
+			case 202: s = "invalid MethodSpec"; break;
+			case 203: s = "invalid FrameExpression"; break;
+			case 204: s = "invalid LabelIdent"; break;
+			case 205: s = "this symbol not expected in FunctionSpec"; break;
+			case 206: s = "invalid FunctionSpec"; break;
+			case 207: s = "invalid PossiblyWildFrameExpression"; break;
+			case 208: s = "invalid PossiblyWildExpression"; break;
+			case 209: s = "this symbol not expected in OneStmt"; break;
+			case 210: s = "invalid OneStmt"; break;
+			case 211: s = "this symbol not expected in OneStmt"; break;
+			case 212: s = "invalid OneStmt"; break;
 			case 213: s = "invalid AssertStmt"; break;
-			case 214: s = "invalid AssumeStmt"; break;
-			case 215: s = "invalid UpdateStmt"; break;
+			case 214: s = "invalid AssertStmt"; break;
+			case 215: s = "invalid AssumeStmt"; break;
 			case 216: s = "invalid UpdateStmt"; break;
-			case 217: s = "this symbol not expected in VarDeclStatement"; break;
-			case 218: s = "invalid VarDeclStatement"; break;
+			case 217: s = "invalid UpdateStmt"; break;
+			case 218: s = "this symbol not expected in VarDeclStatement"; break;
 			case 219: s = "invalid VarDeclStatement"; break;
-			case 220: s = "invalid IfStmt"; break;
+			case 220: s = "invalid VarDeclStatement"; break;
 			case 221: s = "invalid IfStmt"; break;
-			case 222: s = "invalid WhileStmt"; break;
+			case 222: s = "invalid IfStmt"; break;
 			case 223: s = "invalid WhileStmt"; break;
-			case 224: s = "invalid MatchStmt"; break;
-			case 225: s = "invalid ForallStmt"; break;
+			case 224: s = "invalid WhileStmt"; break;
+			case 225: s = "invalid MatchStmt"; break;
 			case 226: s = "invalid ForallStmt"; break;
-			case 227: s = "invalid CalcStmt"; break;
-			case 228: s = "invalid ModifyStmt"; break;
-			case 229: s = "this symbol not expected in ModifyStmt"; break;
-			case 230: s = "invalid ModifyStmt"; break;
-			case 231: s = "invalid ReturnStmt"; break;
-			case 232: s = "invalid Rhs"; break;
+			case 227: s = "invalid ForallStmt"; break;
+			case 228: s = "invalid CalcStmt"; break;
+			case 229: s = "invalid ModifyStmt"; break;
+			case 230: s = "this symbol not expected in ModifyStmt"; break;
+			case 231: s = "invalid ModifyStmt"; break;
+			case 232: s = "invalid ReturnStmt"; break;
 			case 233: s = "invalid Rhs"; break;
-			case 234: s = "invalid Lhs"; break;
-			case 235: s = "invalid NewArray"; break;
-			case 236: s = "invalid CasePatternLocal"; break;
-			case 237: s = "invalid AlternativeBlock"; break;
-			case 238: s = "invalid Guard"; break;
-			case 239: s = "invalid AlternativeBlockCase"; break;
-			case 240: s = "this symbol not expected in AlternativeBlockCase"; break;
+			case 234: s = "invalid Rhs"; break;
+			case 235: s = "invalid Lhs"; break;
+			case 236: s = "invalid NewArray"; break;
+			case 237: s = "invalid CasePatternLocal"; break;
+			case 238: s = "invalid AlternativeBlock"; break;
+			case 239: s = "invalid Guard"; break;
+			case 240: s = "invalid AlternativeBlockCase"; break;
 			case 241: s = "this symbol not expected in AlternativeBlockCase"; break;
-			case 242: s = "this symbol not expected in LoopSpec"; break;
+			case 242: s = "this symbol not expected in AlternativeBlockCase"; break;
 			case 243: s = "this symbol not expected in LoopSpec"; break;
 			case 244: s = "this symbol not expected in LoopSpec"; break;
-			case 245: s = "invalid LoopSpec"; break;
-			case 246: s = "invalid CaseStatement"; break;
-			case 247: s = "this symbol not expected in CaseStatement"; break;
+			case 245: s = "this symbol not expected in LoopSpec"; break;
+			case 246: s = "invalid LoopSpec"; break;
+			case 247: s = "invalid CaseStatement"; break;
 			case 248: s = "this symbol not expected in CaseStatement"; break;
-			case 249: s = "invalid CasePattern"; break;
-			case 250: s = "invalid CalcOp"; break;
-			case 251: s = "invalid EquivOp"; break;
-			case 252: s = "invalid ImpliesOp"; break;
-			case 253: s = "invalid ExpliesOp"; break;
-			case 254: s = "invalid AndOp"; break;
-			case 255: s = "invalid OrOp"; break;
-			case 256: s = "invalid NegOp"; break;
-			case 257: s = "invalid Forall"; break;
-			case 258: s = "invalid Exists"; break;
-			case 259: s = "invalid QSep"; break;
-			case 260: s = "invalid ImpliesExpliesExpression"; break;
-			case 261: s = "invalid LogicalExpression"; break;
+			case 249: s = "this symbol not expected in CaseStatement"; break;
+			case 250: s = "invalid CasePattern"; break;
+			case 251: s = "invalid CalcOp"; break;
+			case 252: s = "invalid EquivOp"; break;
+			case 253: s = "invalid ImpliesOp"; break;
+			case 254: s = "invalid ExpliesOp"; break;
+			case 255: s = "invalid AndOp"; break;
+			case 256: s = "invalid OrOp"; break;
+			case 257: s = "invalid NegOp"; break;
+			case 258: s = "invalid Forall"; break;
+			case 259: s = "invalid Exists"; break;
+			case 260: s = "invalid QSep"; break;
+			case 261: s = "invalid ImpliesExpliesExpression"; break;
 			case 262: s = "invalid LogicalExpression"; break;
-			case 263: s = "invalid ShiftTerm"; break;
-			case 264: s = "invalid RelOp"; break;
-			case 265: s = "invalid AddOp"; break;
-			case 266: s = "invalid BitvectorFactor"; break;
-			case 267: s = "invalid MulOp"; break;
-			case 268: s = "invalid UnaryExpression"; break;
-			case 269: s = "invalid Suffix"; break;
+			case 263: s = "invalid LogicalExpression"; break;
+			case 264: s = "invalid ShiftTerm"; break;
+			case 265: s = "invalid RelOp"; break;
+			case 266: s = "invalid AddOp"; break;
+			case 267: s = "invalid BitvectorFactor"; break;
+			case 268: s = "invalid MulOp"; break;
+			case 269: s = "invalid UnaryExpression"; break;
 			case 270: s = "invalid Suffix"; break;
 			case 271: s = "invalid Suffix"; break;
 			case 272: s = "invalid Suffix"; break;
 			case 273: s = "invalid Suffix"; break;
-			case 274: s = "invalid LambdaExpression"; break;
-			case 275: s = "invalid EndlessExpression"; break;
+			case 274: s = "invalid Suffix"; break;
+			case 275: s = "invalid LambdaExpression"; break;
 			case 276: s = "invalid EndlessExpression"; break;
-			case 277: s = "invalid NameSegment"; break;
-			case 278: s = "invalid DisplayExpr"; break;
-			case 279: s = "invalid MultiSetExpr"; break;
-			case 280: s = "invalid ConstAtomExpression"; break;
-			case 281: s = "invalid Nat"; break;
-			case 282: s = "invalid MatchExpression"; break;
-			case 283: s = "invalid QuantifierGuts"; break;
-			case 284: s = "invalid StmtInExpr"; break;
-			case 285: s = "invalid LetExpr"; break;
-			case 286: s = "invalid CaseExpression"; break;
-			case 287: s = "invalid MemberBindingUpdate"; break;
-			case 288: s = "invalid DotSuffix"; break;
+			case 277: s = "invalid EndlessExpression"; break;
+			case 278: s = "invalid NameSegment"; break;
+			case 279: s = "invalid DisplayExpr"; break;
+			case 280: s = "invalid MultiSetExpr"; break;
+			case 281: s = "invalid ConstAtomExpression"; break;
+			case 282: s = "invalid Nat"; break;
+			case 283: s = "invalid MatchExpression"; break;
+			case 284: s = "invalid QuantifierGuts"; break;
+			case 285: s = "invalid StmtInExpr"; break;
+			case 286: s = "invalid LetExpr"; break;
+			case 287: s = "invalid CaseExpression"; break;
+			case 288: s = "invalid MemberBindingUpdate"; break;
+			case 289: s = "invalid DotSuffix"; break;
 
       default: s = "error " + n; break;
     }
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 35fb1e968e0..06ba0327e82 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -1589,7 +1589,7 @@ public virtual Attributes MergeAttributes(Attributes prevAttrs, Attributes moreA
         return CloneAttributes(prevAttrs);
       } else if (moreAttrs is UserSuppliedAttributes) {
         var usa = (UserSuppliedAttributes)moreAttrs;
-        return new UserSuppliedAttributes(Tok(usa.tok), Tok(usa.OpenBrace), Tok(usa.Colon), Tok(usa.CloseBrace), moreAttrs.Args.ConvertAll(CloneExpr), MergeAttributes(prevAttrs, moreAttrs.Prev));
+        return new UserSuppliedAttributes(Tok(usa.tok), Tok(usa.OpenBrace), Tok(usa.CloseBrace), moreAttrs.Args.ConvertAll(CloneExpr), MergeAttributes(prevAttrs, moreAttrs.Prev));
       } else {
         return new Attributes(moreAttrs.Name, moreAttrs.Args.ConvertAll(CloneExpr), MergeAttributes(prevAttrs, moreAttrs.Prev));
       }
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index f6499656472..13a4fdf894a 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -217,8 +217,8 @@ public override int Read() {
 public class Scanner {
   const char EOL = '\n';
   const int eofSym = 0; /* pdt */
-	const int maxT = 155;
-	const int noSym = 155;
+	const int maxT = 156;
+	const int noSym = 156;
 
 
   [ContractInvariantMethod]
@@ -279,44 +279,44 @@ static Scanner() {
 		start[39] = 58; 
 		start[48] = 59; 
 		start[34] = 27; 
-		start[64] = 105; 
+		start[64] = 106; 
 		start[58] = 60; 
 		start[44] = 34; 
-		start[124] = 106; 
+		start[124] = 107; 
 		start[8226] = 38; 
-		start[46] = 107; 
+		start[46] = 108; 
 		start[96] = 39; 
 		start[59] = 40; 
-		start[61] = 108; 
-		start[123] = 42; 
+		start[61] = 109; 
+		start[123] = 61; 
 		start[125] = 43; 
 		start[91] = 44; 
 		start[93] = 45; 
 		start[40] = 46; 
 		start[41] = 47; 
-		start[60] = 109; 
-		start[62] = 110; 
-		start[33] = 111; 
+		start[60] = 110; 
+		start[62] = 111; 
+		start[33] = 112; 
 		start[8800] = 49; 
 		start[42] = 50; 
-		start[43] = 80; 
-		start[45] = 112; 
-		start[126] = 81; 
-		start[35] = 86; 
-		start[8804] = 88; 
-		start[8805] = 89; 
-		start[8660] = 91; 
-		start[8658] = 93; 
-		start[8656] = 94; 
-		start[38] = 113; 
-		start[8743] = 96; 
-		start[8744] = 98; 
-		start[172] = 99; 
-		start[8704] = 100; 
-		start[8707] = 101; 
-		start[47] = 102; 
-		start[37] = 103; 
-		start[94] = 104; 
+		start[43] = 81; 
+		start[45] = 113; 
+		start[126] = 82; 
+		start[35] = 87; 
+		start[8804] = 89; 
+		start[8805] = 90; 
+		start[8660] = 92; 
+		start[8658] = 94; 
+		start[8656] = 95; 
+		start[38] = 114; 
+		start[8743] = 97; 
+		start[8744] = 99; 
+		start[172] = 100; 
+		start[8704] = 101; 
+		start[8707] = 102; 
+		start[47] = 103; 
+		start[37] = 104; 
+		start[94] = 105; 
 		start[Buffer.EOF] = -1;
 
   }
@@ -573,42 +573,42 @@ public void CheckLiteral() {
 			case "ensures": t.kind = 71; break;
 			case "ghost": t.kind = 72; break;
 			case "witness": t.kind = 73; break;
-			case "reveal": t.kind = 88; break;
-			case "include": t.kind = 89; break;
-			case "abstract": t.kind = 90; break;
-			case "module": t.kind = 91; break;
-			case "refines": t.kind = 92; break;
-			case "opened": t.kind = 93; break;
-			case "provides": t.kind = 95; break;
-			case "reveals": t.kind = 96; break;
-			case "extends": t.kind = 97; break;
-			case "new": t.kind = 98; break;
-			case "yields": t.kind = 99; break;
-			case "returns": t.kind = 100; break;
-			case "comethod": t.kind = 104; break;
-			case "free": t.kind = 105; break;
-			case "yield": t.kind = 106; break;
-			case "label": t.kind = 110; break;
-			case "break": t.kind = 111; break;
-			case "where": t.kind = 112; break;
-			case "return": t.kind = 113; break;
-			case "if": t.kind = 114; break;
-			case "while": t.kind = 115; break;
-			case "match": t.kind = 116; break;
-			case "assert": t.kind = 117; break;
-			case "print": t.kind = 118; break;
-			case "forall": t.kind = 119; break;
-			case "parallel": t.kind = 120; break;
-			case "modify": t.kind = 121; break;
-			case "exists": t.kind = 139; break;
-			case "false": t.kind = 145; break;
-			case "true": t.kind = 146; break;
-			case "null": t.kind = 147; break;
-			case "this": t.kind = 148; break;
-			case "fresh": t.kind = 149; break;
-			case "allocated": t.kind = 150; break;
-			case "unchanged": t.kind = 151; break;
-			case "old": t.kind = 153; break;
+			case "reveal": t.kind = 89; break;
+			case "include": t.kind = 90; break;
+			case "abstract": t.kind = 91; break;
+			case "module": t.kind = 92; break;
+			case "refines": t.kind = 93; break;
+			case "opened": t.kind = 94; break;
+			case "provides": t.kind = 96; break;
+			case "reveals": t.kind = 97; break;
+			case "extends": t.kind = 98; break;
+			case "new": t.kind = 99; break;
+			case "yields": t.kind = 100; break;
+			case "returns": t.kind = 101; break;
+			case "comethod": t.kind = 105; break;
+			case "free": t.kind = 106; break;
+			case "yield": t.kind = 107; break;
+			case "label": t.kind = 111; break;
+			case "break": t.kind = 112; break;
+			case "where": t.kind = 113; break;
+			case "return": t.kind = 114; break;
+			case "if": t.kind = 115; break;
+			case "while": t.kind = 116; break;
+			case "match": t.kind = 117; break;
+			case "assert": t.kind = 118; break;
+			case "print": t.kind = 119; break;
+			case "forall": t.kind = 120; break;
+			case "parallel": t.kind = 121; break;
+			case "modify": t.kind = 122; break;
+			case "exists": t.kind = 140; break;
+			case "false": t.kind = 146; break;
+			case "true": t.kind = 147; break;
+			case "null": t.kind = 148; break;
+			case "this": t.kind = 149; break;
+			case "fresh": t.kind = 150; break;
+			case "allocated": t.kind = 151; break;
+			case "unchanged": t.kind = 152; break;
+			case "old": t.kind = 154; break;
 			default: break;
 		}
   }
@@ -739,7 +739,7 @@ public void CheckLiteral() {
 			case 27:
 				if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 27;}
 				else if (ch == '"') {AddCh(); goto case 33;}
-				else if (ch == 92) {AddCh(); goto case 63;}
+				else if (ch == 92) {AddCh(); goto case 64;}
 				else {goto case 0;}
 			case 28:
 				if (ch >= '0' && ch <= '9' || ch >= 'A' && ch <= 'F' || ch >= 'a' && ch <= 'f') {AddCh(); goto case 29;}
@@ -755,7 +755,7 @@ public void CheckLiteral() {
 				else {goto case 0;}
 			case 32:
 				if (ch <= '!' || ch >= '#' && ch <= 65535) {AddCh(); goto case 32;}
-				else if (ch == '"') {AddCh(); goto case 64;}
+				else if (ch == '"') {AddCh(); goto case 65;}
 				else {goto case 0;}
 			case 33:
 				{t.kind = 24; break;}
@@ -778,21 +778,21 @@ public void CheckLiteral() {
 			case 42:
 				{t.kind = 74; break;}
 			case 43:
-				{t.kind = 75; break;}
-			case 44:
 				{t.kind = 76; break;}
-			case 45:
+			case 44:
 				{t.kind = 77; break;}
-			case 46:
+			case 45:
 				{t.kind = 78; break;}
-			case 47:
+			case 46:
 				{t.kind = 79; break;}
+			case 47:
+				{t.kind = 80; break;}
 			case 48:
-				{t.kind = 83; break;}
-			case 49:
 				{t.kind = 84; break;}
-			case 50:
+			case 49:
 				{t.kind = 85; break;}
+			case 50:
+				{t.kind = 86; break;}
 			case 51:
 				if (ch == 'n') {AddCh(); goto case 52;}
 				else {goto case 0;}
@@ -803,36 +803,36 @@ public void CheckLiteral() {
 				{
 					tlen -= apx;
 					SetScannerBehindT();
-					t.kind = 86; break;}
+					t.kind = 87; break;}
 			case 54:
-				{t.kind = 87; break;}
+				{t.kind = 88; break;}
 			case 55:
 				recEnd = pos; recKind = 2;
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 55;}
-				else if (ch == '_') {AddCh(); goto case 65;}
+				else if (ch == '_') {AddCh(); goto case 66;}
 				else if (ch == '.') {AddCh(); goto case 18;}
 				else {t.kind = 2; break;}
 			case 56:
 				recEnd = pos; recKind = 1;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 2;}
-				else if (ch == 'r') {AddCh(); goto case 66;}
+				else if (ch == 'r') {AddCh(); goto case 67;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
 			case 57:
 				recEnd = pos; recKind = 1;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'u' || ch >= 'w' && ch <= 'z') {AddCh(); goto case 10;}
-				else if (ch == 'v') {AddCh(); goto case 67;}
+				else if (ch == 'v') {AddCh(); goto case 68;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
 			case 58:
 				recEnd = pos; recKind = 1;
-				if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 68;}
-				else if (ch == 39) {AddCh(); goto case 69;}
+				if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 69;}
+				else if (ch == 39) {AddCh(); goto case 70;}
 				else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '&' || ch >= '(' && ch <= '/' || ch >= ':' && ch <= '>' || ch == '@' || ch == '[' || ch >= ']' && ch <= '^' || ch == '`' || ch >= '{' && ch <= 65535) {AddCh(); goto case 21;}
-				else if (ch == 92) {AddCh(); goto case 62;}
+				else if (ch == 92) {AddCh(); goto case 63;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
 			case 59:
 				recEnd = pos; recKind = 2;
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 55;}
-				else if (ch == '_') {AddCh(); goto case 65;}
+				else if (ch == '_') {AddCh(); goto case 66;}
 				else if (ch == 'x') {AddCh(); goto case 15;}
 				else if (ch == '.') {AddCh(); goto case 18;}
 				else {t.kind = 2; break;}
@@ -843,110 +843,112 @@ public void CheckLiteral() {
 				else if (ch == '|') {AddCh(); goto case 37;}
 				else {t.kind = 25; break;}
 			case 61:
+				recEnd = pos; recKind = 75;
+				if (ch == ':') {AddCh(); goto case 42;}
+				else {t.kind = 75; break;}
+			case 62:
 				recEnd = pos; recKind = 1;
-				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 61;}
+				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 62;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
-			case 62:
+			case 63:
 				if (ch == '"' || ch == 39 || ch == '0' || ch == 92 || ch == 'n' || ch == 'r' || ch == 't') {AddCh(); goto case 21;}
 				else if (ch == 'u') {AddCh(); goto case 22;}
 				else {goto case 0;}
-			case 63:
+			case 64:
 				if (ch == '"' || ch == 39 || ch == '0' || ch == 92 || ch == 'n' || ch == 'r' || ch == 't') {AddCh(); goto case 27;}
 				else if (ch == 'u') {AddCh(); goto case 28;}
 				else {goto case 0;}
-			case 64:
+			case 65:
 				recEnd = pos; recKind = 24;
 				if (ch == '"') {AddCh(); goto case 32;}
 				else {t.kind = 24; break;}
-			case 65:
+			case 66:
 				if (ch >= '0' && ch <= '9') {AddCh(); goto case 55;}
 				else {goto case 0;}
-			case 66:
+			case 67:
 				recEnd = pos; recKind = 1;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 3;}
-				else if (ch == 'r') {AddCh(); goto case 70;}
+				else if (ch == 'r') {AddCh(); goto case 71;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
-			case 67:
+			case 68:
 				recEnd = pos; recKind = 1;
 				if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 11;}
-				else if (ch >= '1' && ch <= '9') {AddCh(); goto case 71;}
-				else if (ch == '0') {AddCh(); goto case 72;}
+				else if (ch >= '1' && ch <= '9') {AddCh(); goto case 72;}
+				else if (ch == '0') {AddCh(); goto case 73;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
-			case 68:
+			case 69:
 				recEnd = pos; recKind = 1;
-				if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 73;}
-				else if (ch == 39) {AddCh(); goto case 74;}
+				if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 74;}
+				else if (ch == 39) {AddCh(); goto case 75;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
-			case 69:
+			case 70:
 				recEnd = pos; recKind = 1;
-				if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 73;}
+				if (ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 74;}
 				else if (ch == 39) {AddCh(); goto case 13;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
-			case 70:
+			case 71:
 				recEnd = pos; recKind = 1;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'b' && ch <= 'z') {AddCh(); goto case 4;}
-				else if (ch == 'a') {AddCh(); goto case 75;}
+				else if (ch == 'a') {AddCh(); goto case 76;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
-			case 71:
+			case 72:
 				recEnd = pos; recKind = 7;
-				if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 61;}
-				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 71;}
+				if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 62;}
+				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 72;}
 				else {t.kind = 7; break;}
-			case 72:
+			case 73:
 				recEnd = pos; recKind = 7;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 12;}
 				else {t.kind = 7; break;}
-			case 73:
+			case 74:
 				recEnd = pos; recKind = 1;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 14;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
-			case 74:
+			case 75:
 				recEnd = pos; recKind = 23;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 14;}
 				else {t.kind = 23; break;}
-			case 75:
+			case 76:
 				recEnd = pos; recKind = 1;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'x' || ch == 'z') {AddCh(); goto case 5;}
-				else if (ch == 'y') {AddCh(); goto case 76;}
+				else if (ch == 'y') {AddCh(); goto case 77;}
 				else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
-			case 76:
+			case 77:
 				recEnd = pos; recKind = 5;
 				if (ch == 39 || ch == '0' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 6;}
-				else if (ch >= '1' && ch <= '9') {AddCh(); goto case 77;}
-				else if (ch == '?') {AddCh(); goto case 78;}
+				else if (ch >= '1' && ch <= '9') {AddCh(); goto case 78;}
+				else if (ch == '?') {AddCh(); goto case 79;}
 				else {t.kind = 5; break;}
-			case 77:
+			case 78:
 				recEnd = pos; recKind = 5;
 				if (ch == 39 || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 8;}
-				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 77;}
-				else if (ch == '?') {AddCh(); goto case 79;}
+				else if (ch >= '0' && ch <= '9') {AddCh(); goto case 78;}
+				else if (ch == '?') {AddCh(); goto case 80;}
 				else {t.kind = 5; break;}
-			case 78:
+			case 79:
 				recEnd = pos; recKind = 6;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 7;}
 				else {t.kind = 6; break;}
-			case 79:
+			case 80:
 				recEnd = pos; recKind = 6;
 				if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 9;}
 				else {t.kind = 6; break;}
-			case 80:
-				{t.kind = 101; break;}
 			case 81:
-				if (ch == '>') {AddCh(); goto case 82;}
-				else {goto case 0;}
+				{t.kind = 102; break;}
 			case 82:
-				{t.kind = 107; break;}
-			case 83:
-				if (ch == '>') {AddCh(); goto case 84;}
+				if (ch == '>') {AddCh(); goto case 83;}
 				else {goto case 0;}
-			case 84:
+			case 83:
 				{t.kind = 108; break;}
+			case 84:
+				if (ch == '>') {AddCh(); goto case 85;}
+				else {goto case 0;}
 			case 85:
 				{t.kind = 109; break;}
 			case 86:
-				{t.kind = 122; break;}
+				{t.kind = 110; break;}
 			case 87:
-				{t.kind = 124; break;}
+				{t.kind = 123; break;}
 			case 88:
 				{t.kind = 125; break;}
 			case 89:
@@ -960,7 +962,7 @@ public void CheckLiteral() {
 			case 93:
 				{t.kind = 130; break;}
 			case 94:
-				{t.kind = 132; break;}
+				{t.kind = 131; break;}
 			case 95:
 				{t.kind = 133; break;}
 			case 96:
@@ -974,68 +976,70 @@ public void CheckLiteral() {
 			case 100:
 				{t.kind = 138; break;}
 			case 101:
-				{t.kind = 140; break;}
+				{t.kind = 139; break;}
 			case 102:
 				{t.kind = 141; break;}
 			case 103:
 				{t.kind = 142; break;}
 			case 104:
-				{t.kind = 144; break;}
+				{t.kind = 143; break;}
 			case 105:
-				recEnd = pos; recKind = 152;
-				if (ch == '"') {AddCh(); goto case 32;}
-				else {t.kind = 152; break;}
+				{t.kind = 145; break;}
 			case 106:
+				recEnd = pos; recKind = 153;
+				if (ch == '"') {AddCh(); goto case 32;}
+				else {t.kind = 153; break;}
+			case 107:
 				recEnd = pos; recKind = 27;
-				if (ch == '|') {AddCh(); goto case 97;}
+				if (ch == '|') {AddCh(); goto case 98;}
 				else {t.kind = 27; break;}
-			case 107:
+			case 108:
 				recEnd = pos; recKind = 32;
-				if (ch == '.') {AddCh(); goto case 114;}
+				if (ch == '.') {AddCh(); goto case 115;}
 				else {t.kind = 32; break;}
-			case 108:
-				recEnd = pos; recKind = 94;
-				if (ch == '>') {AddCh(); goto case 41;}
-				else if (ch == '=') {AddCh(); goto case 115;}
-				else {t.kind = 94; break;}
 			case 109:
-				recEnd = pos; recKind = 80;
-				if (ch == '=') {AddCh(); goto case 116;}
-				else {t.kind = 80; break;}
+				recEnd = pos; recKind = 95;
+				if (ch == '>') {AddCh(); goto case 41;}
+				else if (ch == '=') {AddCh(); goto case 116;}
+				else {t.kind = 95; break;}
 			case 110:
 				recEnd = pos; recKind = 81;
-				if (ch == '=') {AddCh(); goto case 87;}
+				if (ch == '=') {AddCh(); goto case 117;}
 				else {t.kind = 81; break;}
 			case 111:
-				recEnd = pos; recKind = 102;
-				if (ch == '=') {AddCh(); goto case 48;}
-				else if (ch == 'i') {AddCh(); goto case 51;}
-				else {t.kind = 102; break;}
+				recEnd = pos; recKind = 82;
+				if (ch == '=') {AddCh(); goto case 88;}
+				else {t.kind = 82; break;}
 			case 112:
 				recEnd = pos; recKind = 103;
-				if (ch == '-') {AddCh(); goto case 83;}
-				else if (ch == '>') {AddCh(); goto case 85;}
+				if (ch == '=') {AddCh(); goto case 48;}
+				else if (ch == 'i') {AddCh(); goto case 51;}
 				else {t.kind = 103; break;}
 			case 113:
-				recEnd = pos; recKind = 143;
-				if (ch == '&') {AddCh(); goto case 95;}
-				else {t.kind = 143; break;}
+				recEnd = pos; recKind = 104;
+				if (ch == '-') {AddCh(); goto case 84;}
+				else if (ch == '>') {AddCh(); goto case 86;}
+				else {t.kind = 104; break;}
 			case 114:
-				recEnd = pos; recKind = 154;
-				if (ch == '.') {AddCh(); goto case 54;}
-				else {t.kind = 154; break;}
+				recEnd = pos; recKind = 144;
+				if (ch == '&') {AddCh(); goto case 96;}
+				else {t.kind = 144; break;}
 			case 115:
-				recEnd = pos; recKind = 82;
-				if (ch == '>') {AddCh(); goto case 92;}
-				else {t.kind = 82; break;}
+				recEnd = pos; recKind = 155;
+				if (ch == '.') {AddCh(); goto case 54;}
+				else {t.kind = 155; break;}
 			case 116:
-				recEnd = pos; recKind = 123;
-				if (ch == '=') {AddCh(); goto case 117;}
-				else {t.kind = 123; break;}
+				recEnd = pos; recKind = 83;
+				if (ch == '>') {AddCh(); goto case 93;}
+				else {t.kind = 83; break;}
 			case 117:
-				recEnd = pos; recKind = 131;
-				if (ch == '>') {AddCh(); goto case 90;}
-				else {t.kind = 131; break;}
+				recEnd = pos; recKind = 124;
+				if (ch == '=') {AddCh(); goto case 118;}
+				else {t.kind = 124; break;}
+			case 118:
+				recEnd = pos; recKind = 132;
+				if (ch == '>') {AddCh(); goto case 91;}
+				else {t.kind = 132; break;}
 
     }
     t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index da23ac3a998..7f6c0f1543c 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -18346,7 +18346,7 @@ public Attributes SubstAttributes(Attributes attrs) {
           if (newArgs != attrs.Args || prev != attrs.Prev) {
             if (attrs is UserSuppliedAttributes) {
               var usa = (UserSuppliedAttributes)attrs;
-              return new UserSuppliedAttributes(usa.tok, usa.OpenBrace, usa.Colon, usa.CloseBrace, newArgs, prev);
+              return new UserSuppliedAttributes(usa.tok, usa.OpenBrace, usa.CloseBrace, newArgs, prev);
             } else {
               return new Attributes(attrs.Name, newArgs, prev);
             }