diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index 31ca38036..59394cee8 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -52,7 +52,7 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
       }
 
       SkipActionDecl = new ActionDecl(Token.NoToken, AddNamePrefix("Skip"), MoverType.Both, new List<Variable>(),
-        new List<Variable>(), true, new List<ActionDeclRef>(), null, null, new List<ElimDecl>(), new List<Requires>(), new List<CallCmd>(),
+        new List<Variable>(), true, new List<ActionDeclRef>(), null, null, new List<Requires>(), new List<CallCmd>(),
         new List<IdentifierExpr>(), null, null);
       var skipImplementation = DeclHelper.Implementation(
         SkipActionDecl,
@@ -146,11 +146,6 @@ private HashSet<ActionDecl> TypeCheckActions()
       {
         SignatureMatcher.CheckSequentializationSignature(actionDecl, actionDecl.RefinedAction.ActionDecl,
           checkingContext);
-        foreach (var elimDecl in actionDecl.Eliminates)
-        {
-          SignatureMatcher.CheckSequentializationSignature(elimDecl.Target.ActionDecl, elimDecl.Abstraction.ActionDecl,
-            checkingContext);
-        }
         if (actionDecl.InvariantAction != null)
         {
           SignatureMatcher.CheckSequentializationSignature(actionDecl, actionDecl.InvariantAction.ActionDecl,
diff --git a/Source/Concurrency/InductiveSequentialization.cs b/Source/Concurrency/InductiveSequentialization.cs
index 67ac58d0b..bc06e3535 100644
--- a/Source/Concurrency/InductiveSequentialization.cs
+++ b/Source/Concurrency/InductiveSequentialization.cs
@@ -9,20 +9,16 @@ public abstract class Sequentialization
   {
     protected CivlTypeChecker civlTypeChecker;
     protected Action targetAction;
-    protected Dictionary<Action, Action> elim;
+    protected HashSet<Action> eliminatedActions;
 
     protected Sequentialization(CivlTypeChecker civlTypeChecker, Action targetAction)
     {
       this.civlTypeChecker = civlTypeChecker;
       this.targetAction = targetAction;
-      this.elim = new Dictionary<Action, Action>(targetAction.ActionDecl.EliminationMap().Select(x =>
-        KeyValuePair.Create(civlTypeChecker.Action(x.Key), civlTypeChecker.Action(x.Value))));
+      this.eliminatedActions = new HashSet<Action>(targetAction.ActionDecl.EliminatedActionDecls().Select(x => civlTypeChecker.Action(x)));
     }
 
-    public IEnumerable<Action> Abstractions => elim.Values;
-
-    private IEnumerable<Tuple<Action, Action>> AbstractionChecks =>
-      elim.Where(kv => kv.Key != kv.Value).Select(kv => Tuple.Create(kv.Key, kv.Value));
+    public IEnumerable<Action> EliminatedActions => eliminatedActions;
 
     public int Layer => targetAction.LayerRange.UpperLayer;
 
@@ -63,29 +59,6 @@ public static void AddCheckers(CivlTypeChecker civlTypeChecker, List<Declaration
       {
         decls.AddRange(x.GenerateCheckers());
       }
-      foreach (var tuple in civlTypeChecker.Sequentializations.SelectMany(x => x.AbstractionChecks).Distinct())
-      {
-        decls.AddRange(GenerateAbstractionChecker(civlTypeChecker, tuple.Item1, tuple.Item2));
-      }
-    }
-
-    private static List<Declaration> GenerateAbstractionChecker(CivlTypeChecker civlTypeChecker, Action action, Action abs)
-    {
-      var requires = abs.Gate.Select(g => new Requires(false, g.Expr)).ToList();
-      // The type checker ensures that the modified set of abs is a subset of the modified set of action.
-      var frame = new HashSet<Variable>(action.ModifiedGlobalVars);
-
-      var subst = action.GetSubstitution(abs);
-      var cmds = action.GetGateAsserts(subst, $"Abstraction {abs.Name} fails gate of {action.Name}").ToList<Cmd>();
-      cmds.Add(CmdHelper.CallCmd(action.Impl.Proc, abs.Impl.InParams, abs.Impl.OutParams));
-      cmds.Add(CmdHelper.AssertCmd(abs.tok, abs.GetTransitionRelation(civlTypeChecker, frame),
-        $"Abstraction {abs.Name} does not summarize {action.Name}"));
-
-      var blocks = new List<Block> { BlockHelper.Block("init", cmds) };
-      var proc = DeclHelper.Procedure(civlTypeChecker.AddNamePrefix($"AbstractionCheck_{action.Name}_{abs.Name}"),
-        abs.Impl.InParams, abs.Impl.OutParams, requires, action.Impl.Proc.Modifies, new List<Ensures>());
-      var impl = DeclHelper.Implementation(proc, proc.InParams, proc.OutParams, new List<Variable>(), blocks);
-      return new List<Declaration>(new Declaration[] { proc, impl });
     }
   }
 
@@ -128,19 +101,18 @@ protected override List<Declaration> GenerateCheckers()
 
     private Implementation CreateInlinedImplementation()
     {
-      var eliminatedActionDecls = targetAction.ActionDecl.EliminationMap();
-      var eliminatedActions = eliminatedActionDecls.Keys.ToHashSet();
+      var eliminatedActionDecls = targetAction.ActionDecl.EliminatedActionDecls();
       var graph = new Graph<ActionDecl>();
-      eliminatedActions.ForEach(actionDecl =>
+      eliminatedActionDecls.ForEach(actionDecl =>
       {
         graph.AddSource(actionDecl);
-        CollectionExtensions.ForEach(actionDecl.CreateActionDecls.Intersect(eliminatedActions), x => graph.AddEdge(x, actionDecl));
+        CollectionExtensions.ForEach(actionDecl.CreateActionDecls.Intersect(eliminatedActionDecls), x => graph.AddEdge(x, actionDecl));
       });
       var eliminatedPendingAsyncs = new Dictionary<CtorType, Implementation>();
       var decls = new List<Declaration>();
       graph.TopologicalSort().ForEach(actionDecl =>
       {
-        var impl = Action.CreateDuplicateImplementation(eliminatedActionDecls[actionDecl].Impl,
+        var impl = Action.CreateDuplicateImplementation(actionDecl.Impl,
           $"{actionDecl.Name}_RefinementCheck");
         eliminatedPendingAsyncs[actionDecl.PendingAsyncType] = impl;
         decls.Add(impl);
@@ -291,41 +263,40 @@ private List<Declaration> GenerateStepChecker(Action pendingAsync)
         Expr.Literal(0))));
       cmds.Add(RemoveChoice(pendingAsyncType));
 
-      Action abs = elim[pendingAsync];
       List<Expr> inputExprs = new List<Expr>();
-      for (int i = 0; i < abs.Impl.InParams.Count; i++)
+      for (int i = 0; i < pendingAsync.Impl.InParams.Count; i++)
       {
         inputExprs.Add(ExprHelper.FieldAccess(Choice(pendingAsyncType), pendingAsyncCtor.InParams[i].Name));
       }
-      cmds.AddRange(abs.GetGateAsserts(Substituter.SubstitutionFromDictionary(abs.Impl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2)),
-        $"Gate of {abs.Name} fails in IS induction step for invariant {invariantAction.Name}"));
-      cmds.AddRange(Preconditions(abs, Substituter.SubstitutionFromDictionary(abs.ActionDecl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2))));
+      cmds.AddRange(pendingAsync.GetGateAsserts(Substituter.SubstitutionFromDictionary(pendingAsync.Impl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2)),
+        $"Gate of {pendingAsync.Name} fails in IS induction step for invariant {invariantAction.Name}"));
+      cmds.AddRange(Preconditions(pendingAsync, Substituter.SubstitutionFromDictionary(pendingAsync.ActionDecl.InParams.Zip(inputExprs).ToDictionary(x => x.Item1, x => x.Item2))));
 
       List<IdentifierExpr> outputExprs = new List<IdentifierExpr>();
-      if (abs.HasPendingAsyncs)
+      if (pendingAsync.HasPendingAsyncs)
       {
-        abs.PendingAsyncs.ForEach(decl =>
+        pendingAsync.PendingAsyncs.ForEach(decl =>
         {
           var ie = NewPAs(decl.PendingAsyncType);
           locals.Add(ie.Decl);
           outputExprs.Add(ie);
         });
       }
-      cmds.Add(CmdHelper.CallCmd(abs.Impl.Proc, inputExprs, outputExprs));
-      if (abs.HasPendingAsyncs)
+      cmds.Add(CmdHelper.CallCmd(pendingAsync.Impl.Proc, inputExprs, outputExprs));
+      if (pendingAsync.HasPendingAsyncs)
       {
-        var lhss = abs.PendingAsyncs.Select(decl => new SimpleAssignLhs(Token.NoToken, PAs(decl.PendingAsyncType)))
+        var lhss = pendingAsync.PendingAsyncs.Select(decl => new SimpleAssignLhs(Token.NoToken, PAs(decl.PendingAsyncType)))
           .ToList<AssignLhs>();
-        var rhss = abs.PendingAsyncs.Select(decl => ExprHelper.FunctionCall(decl.PendingAsyncAdd,
+        var rhss = pendingAsync.PendingAsyncs.Select(decl => ExprHelper.FunctionCall(decl.PendingAsyncAdd,
           PAs(decl.PendingAsyncType), NewPAs(decl.PendingAsyncType))).ToList<Expr>();
         cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
       }
 
       var frame = new HashSet<Variable>(invariantAction.ModifiedGlobalVars);
       cmds.Add(GetCheck(invariantAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame),
-        $"IS step of {invariantAction.Name} with {abs.Name} failed"));
+        $"IS step of {invariantAction.Name} with {pendingAsync.Name} failed"));
 
-      return GetCheckerTuple($"IS_step_{invariantAction.Name}_{abs.Name}", requires,
+      return GetCheckerTuple($"IS_step_{invariantAction.Name}_{pendingAsync.Name}", requires,
         invariantAction.ImplWithChoice.InParams, invariantAction.ImplWithChoice.OutParams, locals, cmds);
     }
 
@@ -374,7 +345,7 @@ public override IEnumerable<Expr> GenerateMoverCheckAssumptions(Action action, L
 
     private Expr ActionExpr(Action action, List<Variable> actionArgs, Substitution invariantFormalSubst)
     {
-      if (!elim.ContainsKey(action))
+      if (!eliminatedActions.Contains(action))
       {
         return Expr.True;
       }
@@ -418,17 +389,16 @@ private Expr ActionExpr(Action action, List<Variable> actionArgs, Substitution i
 
     private Expr LeftMoverExpr(Action leftMover, List<Variable> leftMoverArgs, Substitution invariantFormalSubst)
     {
-      var asyncLeftMover = elim.First(x => x.Value == leftMover).Key;
-      var leftMoverPendingAsyncCtor = asyncLeftMover.ActionDecl.PendingAsyncCtor;
+      var leftMoverPendingAsyncCtor = leftMover.ActionDecl.PendingAsyncCtor;
       var leftMoverPA =
         ExprHelper.FunctionCall(leftMoverPendingAsyncCtor, leftMoverArgs.Select(v => Expr.Ident(v)).ToArray());
       var leftMoverExpr = Expr.And(new[]
       {
-        ChoiceTest(asyncLeftMover.ActionDecl.PendingAsyncType),
+        ChoiceTest(leftMover.ActionDecl.PendingAsyncType),
         Expr.Gt(
-          Expr.Select(PAs(asyncLeftMover.ActionDecl.PendingAsyncType),
-            Choice(asyncLeftMover.ActionDecl.PendingAsyncType)), Expr.Literal(0)),
-        Expr.Eq(Choice(asyncLeftMover.ActionDecl.PendingAsyncType), leftMoverPA)
+          Expr.Select(PAs(leftMover.ActionDecl.PendingAsyncType),
+            Choice(leftMover.ActionDecl.PendingAsyncType)), Expr.Literal(0)),
+        Expr.Eq(Choice(leftMover.ActionDecl.PendingAsyncType), leftMoverPA)
       });
       leftMoverExpr = Substituter.Apply(invariantFormalSubst, leftMoverExpr);
       return leftMoverExpr;
@@ -483,7 +453,7 @@ private Expr NoPendingAsyncs
     {
       get
       {
-        var expr = Expr.And(elim.Keys.Select(action => Expr.Eq(PAs(action.ActionDecl.PendingAsyncType),
+        var expr = Expr.And(eliminatedActions.Select(action => Expr.Eq(PAs(action.ActionDecl.PendingAsyncType),
           ExprHelper.FunctionCall(action.ActionDecl.PendingAsyncConst, Expr.Literal(0)))));
         expr.Typecheck(new TypecheckingContext(null, civlTypeChecker.Options));
         return expr;
@@ -501,7 +471,7 @@ protected override List<Declaration> GenerateCheckers()
       var decls = new List<Declaration>();
       decls.AddRange(GenerateBaseCaseChecker());
       decls.AddRange(GenerateConclusionChecker());
-      foreach (var elim in elim.Keys)
+      foreach (var elim in eliminatedActions)
       {
         decls.AddRange(GenerateStepChecker(elim));
       }
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 883c66a86..d4455d5de 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -83,7 +83,7 @@ where first.IsRightMover || second.IsLeftMover
 
       foreach (var sequentialization in civlTypeChecker.Sequentializations)
       {
-        foreach (var leftMover in sequentialization.Abstractions)
+        foreach (var leftMover in sequentialization.EliminatedActions)
         {
           foreach (var action in civlTypeChecker.MoverActions.Where(x => x.LayerRange.Contains(sequentialization.Layer)))
           {
diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
index 795067855..f04a317bb 100644
--- a/Source/Core/AST/Absy.cs
+++ b/Source/Core/AST/Absy.cs
@@ -2909,36 +2909,12 @@ public enum MoverType
     None
   }
 
-  public class ElimDecl : Absy
-  {
-    public ActionDeclRef Target;
-    public ActionDeclRef Abstraction;
-
-    public ElimDecl(IToken tok, ActionDeclRef target, ActionDeclRef abstraction) : base(tok)
-    {
-      this.Target = target;
-      this.Abstraction = abstraction;
-    }
-
-    public override void Resolve(ResolutionContext rc)
-    {
-      Target.Resolve(rc);
-      Abstraction.Resolve(rc);
-    }
-
-    public override void Typecheck(TypecheckingContext tc)
-    {
-      throw new NotImplementedException();
-    }
-  }
-
   public class ActionDecl : Procedure
   {
     public MoverType MoverType;
     public List<ActionDeclRef> Creates;
     public ActionDeclRef RefinedAction;
     public ActionDeclRef InvariantAction;
-    public List<ElimDecl> Eliminates;
     public List<CallCmd> YieldRequires;
     public DatatypeTypeCtorDecl PendingAsyncCtorDecl;
 
@@ -2948,7 +2924,7 @@ public class ActionDecl : Procedure
     public ActionDecl(IToken tok, string name, MoverType moverType,
       List<Variable> inParams, List<Variable> outParams, bool isPure,
       List<ActionDeclRef> creates, ActionDeclRef refinedAction, ActionDeclRef invariantAction,
-      List<ElimDecl> eliminates, List<Requires> requires, List<CallCmd> yieldRequires,
+      List<Requires> requires, List<CallCmd> yieldRequires,
       List<IdentifierExpr> modifies, DatatypeTypeCtorDecl pendingAsyncCtorDecl, QKeyValue kv) : base(tok, name,
       new List<TypeVariable>(), inParams, outParams,
       isPure, requires, modifies, new List<Ensures>(), kv)
@@ -2957,7 +2933,6 @@ public ActionDecl(IToken tok, string name, MoverType moverType,
       this.Creates = creates;
       this.RefinedAction = refinedAction;
       this.InvariantAction = invariantAction;
-      this.Eliminates = eliminates;
       this.YieldRequires = yieldRequires;
       this.PendingAsyncCtorDecl = pendingAsyncCtorDecl;
     }
@@ -3018,21 +2993,6 @@ public override void Resolve(ResolutionContext rc)
       {
         InvariantAction.Resolve(rc);
       }
-      Eliminates.ForEach(elim =>
-      {
-        elim.Resolve(rc);
-      });
-      if (Eliminates.Any())
-      {
-        if (RefinedAction == null)
-        {
-          rc.Error(this, "eliminates clause must be accompanied by refinement specification");
-        }
-        if (Eliminates.Select(elim => elim.Target.ActionDecl).Distinct().Count() != Eliminates.Count)
-        {
-          rc.Error(this, "each eliminates pair must be distinct in the first action");
-        }
-      }
     }
 
     public override void Typecheck(TypecheckingContext tc)
@@ -3109,26 +3069,6 @@ public override void Typecheck(TypecheckingContext tc)
               tc.Error(this, $"modifies of {elimProc.Name} must be subset of modifies of {invariantActionDecl.Name}");
             }
           }
-          foreach (var elimDecl in Eliminates)
-          {
-            var targetActionDecl = elimDecl.Target.ActionDecl;
-            var abstractionActionDecl = elimDecl.Abstraction.ActionDecl;
-            var targetModifies = new HashSet<Variable>(targetActionDecl.Modifies.Select(ie => ie.Decl));
-            var absModifies = new HashSet<Variable>(abstractionActionDecl.Modifies.Select(ie => ie.Decl));
-            if (!invariantCreates.Contains(targetActionDecl))
-            {
-              tc.Error(this, $"eliminated action must be created by invariant {InvariantAction.ActionName}");
-            }
-            if (!abstractionActionDecl.LayerRange.Contains(layer))
-            {
-              tc.Error(elimDecl, $"action {abstractionActionDecl.Name} does not exist at layer {layer}");
-            }
-            if (!absModifies.IsSubsetOf(targetModifies))
-            {
-              tc.Error(elimDecl,
-                $"modifies of {abstractionActionDecl.Name} must be subset of modifies of {targetActionDecl.Name}");
-            }
-          }
         }
       }
     }
@@ -3185,7 +3125,7 @@ protected override void EmitEnd(TokenTextWriter stream, int level)
       base.EmitEnd(stream, level);
     }
 
-    public Dictionary<ActionDecl, ActionDecl> EliminationMap()
+    public IEnumerable<ActionDecl> EliminatedActionDecls()
     {
       var refinedProc = RefinedAction.ActionDecl;
       var refinedActionCreates = refinedProc.CreateActionDecls.ToHashSet();
@@ -3202,13 +3142,8 @@ HashSet<ActionDecl> FixpointCreates()
       }
       var allCreates = InvariantAction == null
         ? FixpointCreates()
-        : InvariantAction.ActionDecl.CreateActionDecls.ToHashSet();
-      var elimMap = allCreates.Except(refinedActionCreates).ToDictionary(x => x, x => x);
-      foreach (var elimDecl in Eliminates)
-      {
-        elimMap[elimDecl.Target.ActionDecl] = elimDecl.Abstraction.ActionDecl;
-      }
-      return elimMap;
+        : InvariantAction.ActionDecl.CreateActionDecls;
+      return allCreates.Except(refinedActionCreates);
     }
 
     public IEnumerable<ActionDeclRef> ActionDeclRefs()
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 0e168be20..1de9339fd 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -670,7 +670,6 @@ ActionDecl<bool isPure, out ActionDecl actionDecl, out Implementation impl, out
      List<ActionDeclRef> creates = new List<ActionDeclRef>();
      ActionDeclRef refinedAction = null;
      ActionDeclRef invariantAction = null;
-     List<ElimDecl> elims = new List<ElimDecl>();
      List<Requires> requires = new List<Requires>();
      List<CallCmd> yieldRequires = new List<CallCmd>();
      List<Variable> locals;
@@ -687,8 +686,8 @@ ActionDecl<bool isPure, out ActionDecl actionDecl, out Implementation impl, out
   ProcFormals<true, true, out ins>
     [ "returns" ProcFormals<false, true, out outs> ]
   ( ";"
-    { SpecAction<ref refinedAction, ref invariantAction, mods, creates, elims, requires, yieldRequires> }
-  | { SpecAction<ref refinedAction, ref invariantAction, mods, creates, elims, requires, yieldRequires> }
+    { SpecAction<ref refinedAction, ref invariantAction, mods, creates, requires, yieldRequires> }
+  | { SpecAction<ref refinedAction, ref invariantAction, mods, creates, requires, yieldRequires> }
     ImplBody<out locals, out stmtList>
     (.
        impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
@@ -722,7 +721,7 @@ ActionDecl<bool isPure, out ActionDecl actionDecl, out Implementation impl, out
          datatypeTypeCtorDecl.AddConstructor(name, name.val, fields);
        }
      }
-     actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, requires, yieldRequires, mods, datatypeTypeCtorDecl, kv);
+     actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, requires, yieldRequires, mods, datatypeTypeCtorDecl, kv);
   .)
   .
 
@@ -733,19 +732,6 @@ SpecCreates<.List<ActionDeclRef> creates.>
   ";"
   .
 
-SpecUsing<.List<ElimDecl> elims.>
-= (. IToken name, tok; ActionDeclRef target, abstraction; .)
-  Ident<out name> (. target = new ActionDeclRef(name, name.val); .)
-  "using" (. tok = t; .)
-  Ident<out name> (. abstraction = new ActionDeclRef(name, name.val); .)
-  (. elims.Add(new ElimDecl(tok, target, abstraction)); .)
-  .
-
-SpecEliminates<.List<ElimDecl> elims.>
-=
-  "eliminates" SpecUsing<elims> { "," SpecUsing<elims> } ";"
-  .
-
 SpecRefinedAction<ref ActionDeclRef refinedAction>
 =
   "refines" (. IToken m; .) Ident<out m>
@@ -758,7 +744,7 @@ SpecRefinedAction<ref ActionDeclRef refinedAction>
   .)
   .
 
-SpecAction<.ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<ElimDecl> elims, List<Requires> requires, List<CallCmd> yieldRequires.>
+SpecAction<.ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<Requires> requires, List<CallCmd> yieldRequires.>
 =
   (
     SpecRefinedAction<ref refinedAction>
@@ -767,7 +753,6 @@ SpecAction<.ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction,
     ";"
   | SpecModifies<mods>
   | SpecCreates<creates>
-  | SpecEliminates<elims>
   | SpecYieldRequires<requires, yieldRequires>
   )
   .
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 3354a60a1..4633afef4 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -483,16 +483,6 @@ public override Procedure VisitProcedure(Procedure node)
       return newProcedure;
     }
 
-    public override ElimDecl VisitElimDecl(ElimDecl node)
-    {
-      return base.VisitElimDecl((ElimDecl)node.Clone());
-    }
-
-    public override List<ElimDecl> VisitElimDeclSeq(List<ElimDecl> node)
-    {
-      return base.VisitElimDeclSeq(new List<ElimDecl>(node));
-    }
-
     // We duplicate ActionDecl's but we are not updating references to ActionDecl
     // in ActionDeclRef instances. If ActionDeclRef instances need to be updated,
     // override VisitActionDeclRef appropriately.
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 561bbf08c..1b2da262c 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -36,7 +36,7 @@ public class Parser {
 	public const int _decimal = 5;
 	public const int _dec_float = 6;
 	public const int _float = 7;
-	public const int maxT = 119;
+	public const int maxT = 118;
 
 	const bool _T = true;
 	const bool _x = false;
@@ -304,12 +304,12 @@ void BoogiePL() {
 					 Pgm.AddTopLevelDeclaration(im);
 					}
 					
-				} else SynErr(120);
+				} else SynErr(119);
 				break;
 			}
-			case 35: case 36: case 37: case 42: case 43: case 44: case 45: case 46: {
+			case 35: case 36: case 37: case 41: case 42: case 43: case 44: case 45: {
 				Pure(ref isPure);
-				if (la.kind == 46) {
+				if (la.kind == 45) {
 					Procedure(isPure, out pr, out im);
 					Pgm.AddTopLevelDeclaration(pr);
 					if (im != null) {
@@ -328,10 +328,10 @@ void BoogiePL() {
 					}
 					isPure = false;
 					
-				} else SynErr(121);
+				} else SynErr(120);
 				break;
 			}
-			case 50: {
+			case 49: {
 				Implementation(out nnim);
 				Pgm.AddTopLevelDeclaration(nnim); 
 				break;
@@ -367,7 +367,7 @@ void Consts(out List<Declaration>/*!*/ ds) {
 				axioms.Add(axiom); ds.Add(axiom); 
 			}
 			Expect(27);
-		} else SynErr(122);
+		} else SynErr(121);
 		foreach(TypedIdent/*!*/ x in xs){
 		 Contract.Assert(x != null);
 		 var constant = new Constant(y, x, u, kv, axioms);
@@ -421,7 +421,7 @@ void Function(out List<Declaration>/*!*/ ds) {
 			Get();
 			Type(out retTy);
 			retTyd = new TypedIdent(retTy.tok, TypedIdent.NoName, retTy); 
-		} else SynErr(123);
+		} else SynErr(122);
 		if (la.kind == 26) {
 			Get();
 			Expression(out tmp);
@@ -446,7 +446,7 @@ void Function(out List<Declaration>/*!*/ ds) {
 			Expect(27);
 		} else if (la.kind == 10) {
 			Get();
-		} else SynErr(124);
+		} else SynErr(123);
 		if (retTyd == null) {
 		 // construct a dummy type for the case of syntax error
 		 retTyd = new TypedIdent(t, TypedIdent.NoName, new BasicType(t, SimpleType.Int));
@@ -602,7 +602,7 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl)
 		if (StartOf(5)) {
 			MoverQualifier(ref moverType);
 		}
-		Expect(46);
+		Expect(45);
 		while (la.kind == 26) {
 			Attribute(ref kv);
 		}
@@ -625,7 +625,7 @@ void YieldProcedureDecl(out YieldProcedureDecl ypDecl, out Implementation impl)
 			impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
 			                         locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
 			
-		} else SynErr(125);
+		} else SynErr(124);
 		ypDecl = new YieldProcedureDecl(name, name.val, moverType, ins, outs, pre, mods, post, yieldRequires, yieldEnsures, yieldPreserves, refinedAction, kv); 
 	}
 
@@ -648,7 +648,7 @@ void Procedure(bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implemen
 		QKeyValue kv = null;
 		impl = null;
 		
-		Expect(46);
+		Expect(45);
 		ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
 		if (la.kind == 10) {
 			Get();
@@ -663,7 +663,7 @@ void Procedure(bool isPure, out Procedure/*!*/ proc, out /*maybe null*/ Implemen
 			impl = new Implementation(x, x.val, typeParams.ConvertAll(tp => new TypeVariable(tp.tok, tp.Name)),
 			                         Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
 			
-		} else SynErr(126);
+		} else SynErr(125);
 		proc = new Procedure(x, x.val, typeParams, ins, outs, isPure, pre, mods, post, kv); 
 	}
 
@@ -676,7 +676,6 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl,
 		List<ActionDeclRef> creates = new List<ActionDeclRef>();
 		ActionDeclRef refinedAction = null;
 		ActionDeclRef invariantAction = null;
-		List<ElimDecl> elims = new List<ElimDecl>();
 		List<Requires> requires = new List<Requires>();
 		List<CallCmd> yieldRequires = new List<CallCmd>();
 		List<Variable> locals;
@@ -705,17 +704,17 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl,
 		if (la.kind == 10) {
 			Get();
 			while (StartOf(10)) {
-				SpecAction(ref refinedAction, ref invariantAction, mods, creates, elims, requires, yieldRequires);
+				SpecAction(ref refinedAction, ref invariantAction, mods, creates, requires, yieldRequires);
 			}
 		} else if (StartOf(11)) {
 			while (StartOf(10)) {
-				SpecAction(ref refinedAction, ref invariantAction, mods, creates, elims, requires, yieldRequires);
+				SpecAction(ref refinedAction, ref invariantAction, mods, creates, requires, yieldRequires);
 			}
 			ImplBody(out locals, out stmtList);
 			impl = new Implementation(name, name.val, new List<TypeVariable>(), Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs),
 			                              locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
 			
-		} else SynErr(127);
+		} else SynErr(126);
 		if (isPure) {
 		 if (moverType == MoverType.None)
 		 {
@@ -742,7 +741,7 @@ void ActionDecl(bool isPure, out ActionDecl actionDecl, out Implementation impl,
 		   datatypeTypeCtorDecl.AddConstructor(name, name.val, fields);
 		 }
 		}
-		actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, elims, requires, yieldRequires, mods, datatypeTypeCtorDecl, kv);
+		actionDecl = new ActionDecl(name, name.val, moverType, ins, outs, isPure, creates, refinedAction, invariantAction, requires, yieldRequires, mods, datatypeTypeCtorDecl, kv);
 		
 	}
 
@@ -754,7 +753,7 @@ void Implementation(out Implementation/*!*/ impl) {
 		StmtList/*!*/ stmtList;
 		QKeyValue kv;
 		
-		Expect(50);
+		Expect(49);
 		ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
 		ImplBody(out locals, out stmtList);
 		impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); 
@@ -853,7 +852,7 @@ void Type(out Bpl.Type/*!*/ ty) {
 			ty = new UnresolvedTypeIdentifier (tok, tok.val, args); 
 		} else if (la.kind == 19 || la.kind == 21) {
 			MapType(out ty);
-		} else SynErr(128);
+		} else SynErr(127);
 	}
 
 	void AttributesIdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIdent, QKeyValue> action ) {
@@ -889,7 +888,7 @@ void IdsTypeWhere(bool allowWhereClauses, string context, System.Action<TypedIde
 	void Expression(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		ImpliesExpression(false, out e0);
-		while (la.kind == 68 || la.kind == 69) {
+		while (la.kind == 67 || la.kind == 68) {
 			EquivOp();
 			x = t; 
 			ImpliesExpression(false, out e1);
@@ -912,26 +911,26 @@ void TypeAtom(out Bpl.Type/*!*/ ty) {
 			Get();
 			Type(out ty);
 			Expect(12);
-		} else SynErr(129);
+		} else SynErr(128);
 	}
 
 	void Ident(out IToken/*!*/ x) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null);
 		if (la.kind == 1) {
 			Get();
-		} else if (la.kind == 45) {
+		} else if (la.kind == 44) {
 			Get();
 			t.kind = _ident; 
-		} else if (la.kind == 44) {
+		} else if (la.kind == 43) {
 			Get();
 			t.kind = _ident; 
-		} else if (la.kind == 42) {
+		} else if (la.kind == 41) {
 			Get();
 			t.kind = _ident; 
-		} else if (la.kind == 43) {
+		} else if (la.kind == 42) {
 			Get();
 			t.kind = _ident; 
-		} else SynErr(130);
+		} else SynErr(129);
 		x = t;
 		if (x.val.StartsWith("\\"))
 		 x.val = x.val.Substring(1);
@@ -956,7 +955,7 @@ void TypeArgs(List<Bpl.Type>/*!*/ ts) {
 		} else if (la.kind == 19 || la.kind == 21) {
 			MapType(out ty);
 			ts.Add(ty); 
-		} else SynErr(131);
+		} else SynErr(130);
 	}
 
 	void MapType(out Bpl.Type/*!*/ ty) {
@@ -1105,40 +1104,38 @@ void Invariant(List<Requires> invariants) {
 	}
 
 	void MoverQualifier(ref MoverType moverType) {
-		if (la.kind == 42) {
+		if (la.kind == 41) {
 			Get();
 			moverType = MoverType.Left; 
-		} else if (la.kind == 43) {
+		} else if (la.kind == 42) {
 			Get();
 			moverType = MoverType.Right; 
-		} else if (la.kind == 44) {
+		} else if (la.kind == 43) {
 			Get();
 			moverType = MoverType.Both; 
-		} else if (la.kind == 45) {
+		} else if (la.kind == 44) {
 			Get();
 			moverType = MoverType.Atomic; 
-		} else SynErr(132);
+		} else SynErr(131);
 	}
 
-	void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<ElimDecl> elims, List<Requires> requires, List<CallCmd> yieldRequires) {
-		if (la.kind == 41) {
+	void SpecAction(ref ActionDeclRef refinedAction, ref ActionDeclRef invariantAction, List<IdentifierExpr> mods, List<ActionDeclRef> creates, List<Requires> requires, List<CallCmd> yieldRequires) {
+		if (la.kind == 39) {
 			SpecRefinedAction(ref refinedAction);
 			IToken m; 
-			if (la.kind == 39) {
+			if (la.kind == 40) {
 				Get();
 				Ident(out m);
 				invariantAction = new ActionDeclRef(m, m.val); 
 			}
 			Expect(10);
-		} else if (la.kind == 52) {
+		} else if (la.kind == 51) {
 			SpecModifies(mods);
 		} else if (la.kind == 38) {
 			SpecCreates(creates);
-		} else if (la.kind == 40) {
-			SpecEliminates(elims);
-		} else if (la.kind == 47) {
+		} else if (la.kind == 46) {
 			SpecYieldRequires(requires, yieldRequires);
-		} else SynErr(133);
+		} else SynErr(132);
 	}
 
 	void ImplBody(out List<Variable>/*!*/ locals, out StmtList/*!*/ stmtList) {
@@ -1158,29 +1155,8 @@ void SpecCreates(List<ActionDeclRef> creates) {
 		Expect(10);
 	}
 
-	void SpecUsing(List<ElimDecl> elims) {
-		IToken name, tok; ActionDeclRef target, abstraction; 
-		Ident(out name);
-		target = new ActionDeclRef(name, name.val); 
-		Expect(39);
-		tok = t; 
-		Ident(out name);
-		abstraction = new ActionDeclRef(name, name.val); 
-		elims.Add(new ElimDecl(tok, target, abstraction)); 
-	}
-
-	void SpecEliminates(List<ElimDecl> elims) {
-		Expect(40);
-		SpecUsing(elims);
-		while (la.kind == 14) {
-			Get();
-			SpecUsing(elims);
-		}
-		Expect(10);
-	}
-
 	void SpecRefinedAction(ref ActionDeclRef refinedAction) {
-		Expect(41);
+		Expect(39);
 		IToken m; 
 		Ident(out m);
 		if (refinedAction == null) {
@@ -1193,7 +1169,7 @@ void SpecRefinedAction(ref ActionDeclRef refinedAction) {
 
 	void SpecModifies(List<IdentifierExpr> mods) {
 		List<IToken> ms; 
-		Expect(52);
+		Expect(51);
 		if (StartOf(14)) {
 			Idents(out ms);
 			foreach(IToken m in ms) { mods.Add(new IdentifierExpr(m, m.val)); } 
@@ -1203,7 +1179,7 @@ void SpecModifies(List<IdentifierExpr> mods) {
 
 	void SpecYieldRequires(List<Requires> pre, List<CallCmd> yieldRequires ) {
 		Expr e; Cmd cmd; Token tok; QKeyValue kv = null; 
-		Expect(47);
+		Expect(46);
 		tok = t; 
 		if (StartOf(16)) {
 			while (la.kind == 26) {
@@ -1211,26 +1187,26 @@ void SpecYieldRequires(List<Requires> pre, List<CallCmd> yieldRequires ) {
 			}
 			Proposition(out e);
 			pre.Add(new Requires(tok, false, e, null, kv)); 
-		} else if (la.kind == 36 || la.kind == 51 || la.kind == 65) {
+		} else if (la.kind == 36 || la.kind == 50 || la.kind == 64) {
 			CallCmd(out cmd);
 			yieldRequires.Add((CallCmd)cmd); 
-		} else SynErr(134);
+		} else SynErr(133);
 		Expect(10);
 	}
 
 	void SpecYieldPrePost(ref ActionDeclRef refinedAction, List<Requires> pre, List<Ensures> post, List<CallCmd> yieldRequires, List<CallCmd> yieldEnsures, List<CallCmd> yieldPreserves, List<IdentifierExpr> mods) {
-		if (la.kind == 41) {
+		if (la.kind == 39) {
 			SpecRefinedAction(ref refinedAction);
 			Expect(10);
-		} else if (la.kind == 47) {
+		} else if (la.kind == 46) {
 			SpecYieldRequires(pre, yieldRequires);
-		} else if (la.kind == 48) {
+		} else if (la.kind == 47) {
 			SpecYieldEnsures(post, yieldEnsures);
-		} else if (la.kind == 49) {
+		} else if (la.kind == 48) {
 			SpecYieldPreserves(yieldPreserves);
-		} else if (la.kind == 52) {
+		} else if (la.kind == 51) {
 			SpecModifies(mods);
-		} else SynErr(135);
+		} else SynErr(134);
 	}
 
 	void CallCmd(out Cmd c) {
@@ -1244,11 +1220,11 @@ void CallCmd(out Cmd c) {
 			Get();
 			isAsync = true; 
 		}
-		if (la.kind == 51) {
+		if (la.kind == 50) {
 			Get();
 			isFree = true; 
 		}
-		Expect(65);
+		Expect(64);
 		x = t; 
 		CallParams(isAsync, isFree, x, out c);
 		
@@ -1256,7 +1232,7 @@ void CallCmd(out Cmd c) {
 
 	void SpecYieldEnsures(List<Ensures> post, List<CallCmd> yieldEnsures ) {
 		Expr e; Cmd cmd; Token tok; QKeyValue kv = null; 
-		Expect(48);
+		Expect(47);
 		tok = t; 
 		if (StartOf(16)) {
 			while (la.kind == 26) {
@@ -1264,16 +1240,16 @@ void SpecYieldEnsures(List<Ensures> post, List<CallCmd> yieldEnsures ) {
 			}
 			Proposition(out e);
 			post.Add(new Ensures(tok, false, e, null, kv)); 
-		} else if (la.kind == 36 || la.kind == 51 || la.kind == 65) {
+		} else if (la.kind == 36 || la.kind == 50 || la.kind == 64) {
 			CallCmd(out cmd);
 			yieldEnsures.Add((CallCmd)cmd); 
-		} else SynErr(136);
+		} else SynErr(135);
 		Expect(10);
 	}
 
 	void SpecYieldPreserves(List<CallCmd> yieldPreserves ) {
 		Cmd cmd; Token tok; 
-		Expect(49);
+		Expect(48);
 		tok = t; 
 		CallCmd(out cmd);
 		yieldPreserves.Add((CallCmd)cmd); 
@@ -1300,19 +1276,19 @@ void ProcSignature(bool allowWhereClausesOnFormals, out IToken/*!*/ name, out Li
 	}
 
 	void Spec(List<Requires> pre, List<IdentifierExpr> mods, List<Ensures> post) {
-		if (la.kind == 52) {
+		if (la.kind == 51) {
 			SpecModifies(mods);
-		} else if (la.kind == 51) {
+		} else if (la.kind == 50) {
 			Get();
 			SpecPrePost(true, pre, post);
-		} else if (la.kind == 47 || la.kind == 48) {
+		} else if (la.kind == 46 || la.kind == 47) {
 			SpecPrePost(false, pre, post);
-		} else SynErr(137);
+		} else SynErr(136);
 	}
 
 	void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 		Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; 
-		if (la.kind == 47) {
+		if (la.kind == 46) {
 			Get();
 			tok = t; 
 			while (la.kind == 26) {
@@ -1321,7 +1297,7 @@ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 			Proposition(out e);
 			Expect(10);
 			pre.Add(new Requires(tok, free, e, null, kv)); 
-		} else if (la.kind == 48) {
+		} else if (la.kind == 47) {
 			Get();
 			tok = t; 
 			while (la.kind == 26) {
@@ -1330,7 +1306,7 @@ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
 			Proposition(out e);
 			Expect(10);
 			post.Add(new Ensures(tok, free, e, null, kv)); 
-		} else SynErr(138);
+		} else SynErr(137);
 	}
 
 	void StmtList(out StmtList/*!*/ stmtList) {
@@ -1366,7 +1342,7 @@ void StmtList(out StmtList/*!*/ stmtList) {
 				 cs = new List<Cmd>();
 				}
 				
-			} else if (la.kind == 55 || la.kind == 57 || la.kind == 59) {
+			} else if (la.kind == 54 || la.kind == 56 || la.kind == 58) {
 				StructuredCmd(out ecn);
 				ec = ecn;
 				if (startToken == null) { startToken = ec.tok;  cs = new List<Cmd>(); }
@@ -1410,11 +1386,11 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 		QKeyValue kv = null;
 		
 		switch (la.kind) {
-		case 1: case 42: case 43: case 44: case 45: {
+		case 1: case 41: case 42: case 43: case 44: {
 			LabelOrAssign(out c, out label);
 			break;
 		}
-		case 60: {
+		case 59: {
 			Get();
 			x = t; 
 			while (la.kind == 26) {
@@ -1425,7 +1401,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			Expect(10);
 			break;
 		}
-		case 61: {
+		case 60: {
 			Get();
 			x = t; 
 			while (la.kind == 26) {
@@ -1436,7 +1412,7 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			Expect(10);
 			break;
 		}
-		case 62: {
+		case 61: {
 			Get();
 			x = t; 
 			Idents(out xs);
@@ -1450,18 +1426,18 @@ void LabelOrCmd(out Cmd c, out IToken label) {
 			
 			break;
 		}
-		case 36: case 51: case 65: {
+		case 36: case 50: case 64: {
 			CallCmd(out cn);
 			Expect(10);
 			c = cn; 
 			break;
 		}
-		case 66: {
+		case 65: {
 			ParCallCmd(out cn);
 			c = cn; 
 			break;
 		}
-		default: SynErr(139); break;
+		default: SynErr(138); break;
 		}
 	}
 
@@ -1469,16 +1445,16 @@ void StructuredCmd(out StructuredCmd/*!*/ ec) {
 		Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd;  Contract.Assume(cce.IsPeerConsistent(ec));
 		IfCmd/*!*/ ifcmd;  WhileCmd/*!*/ wcmd;  BreakCmd/*!*/ bcmd;
 		
-		if (la.kind == 55) {
+		if (la.kind == 54) {
 			IfCmd(out ifcmd);
 			ec = ifcmd; 
-		} else if (la.kind == 57) {
+		} else if (la.kind == 56) {
 			WhileCmd(out wcmd);
 			ec = wcmd; 
-		} else if (la.kind == 59) {
+		} else if (la.kind == 58) {
 			BreakCmd(out bcmd);
 			ec = bcmd; 
-		} else SynErr(140);
+		} else SynErr(139);
 	}
 
 	void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1486,7 +1462,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) {
 		Token y;  List<IToken>/*!*/ xs;
 		List<String> ss = new List<String>();
 		
-		if (la.kind == 53) {
+		if (la.kind == 52) {
 			Get();
 			y = t; 
 			Idents(out xs);
@@ -1495,10 +1471,10 @@ void TransferCmd(out TransferCmd/*!*/ tc) {
 			 ss.Add(s.val); }
 			tc = new GotoCmd(y, ss);
 			
-		} else if (la.kind == 54) {
+		} else if (la.kind == 53) {
 			Get();
 			tc = new ReturnCmd(t); 
-		} else SynErr(141);
+		} else SynErr(140);
 		Expect(10);
 	}
 
@@ -1509,21 +1485,21 @@ void IfCmd(out IfCmd/*!*/ ifcmd) {
 		IfCmd/*!*/ elseIf;  IfCmd elseIfOption = null;
 		StmtList/*!*/ els;  StmtList elseOption = null;
 		
-		Expect(55);
+		Expect(54);
 		x = t; 
 		Guard(out guard);
 		Expect(26);
 		StmtList(out thn);
-		if (la.kind == 56) {
+		if (la.kind == 55) {
 			Get();
-			if (la.kind == 55) {
+			if (la.kind == 54) {
 				IfCmd(out elseIf);
 				elseIfOption = elseIf; 
 			} else if (la.kind == 26) {
 				Get();
 				StmtList(out els);
 				elseOption = els; 
-			} else SynErr(142);
+			} else SynErr(141);
 		}
 		ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); 
 	}
@@ -1536,13 +1512,13 @@ void WhileCmd(out WhileCmd wcmd) {
 		StmtList body;
 		QKeyValue kv = null;
 		
-		Expect(57);
+		Expect(56);
 		x = t; 
 		Guard(out guard);
 		Contract.Assume(guard == null || cce.Owner.None(guard)); 
-		while (la.kind == 34 || la.kind == 51) {
+		while (la.kind == 34 || la.kind == 50) {
 			isFree = false; z = la/*lookahead token*/; 
-			if (la.kind == 51) {
+			if (la.kind == 50) {
 				Get();
 				isFree = true;  
 			}
@@ -1559,10 +1535,10 @@ void WhileCmd(out WhileCmd wcmd) {
 				}
 				kv = null;
 				
-			} else if (la.kind == 36 || la.kind == 51 || la.kind == 65) {
+			} else if (la.kind == 36 || la.kind == 50 || la.kind == 64) {
 				CallCmd(out cmd);
 				yields.Add((CallCmd)cmd); 
-			} else SynErr(143);
+			} else SynErr(142);
 			Expect(10);
 		}
 		Expect(26);
@@ -1574,7 +1550,7 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) {
 		Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x;  IToken/*!*/ y;
 		string breakLabel = null;
 		
-		Expect(59);
+		Expect(58);
 		x = t; 
 		if (StartOf(14)) {
 			Ident(out y);
@@ -1587,13 +1563,13 @@ void BreakCmd(out BreakCmd/*!*/ bcmd) {
 	void Guard(out Expr e) {
 		Expr/*!*/ ee;  e = null; 
 		Expect(11);
-		if (la.kind == 58) {
+		if (la.kind == 57) {
 			Get();
 			e = null; 
 		} else if (StartOf(19)) {
 			Expression(out ee);
 			e = ee; 
-		} else SynErr(144);
+		} else SynErr(143);
 		Expect(12);
 	}
 
@@ -1619,7 +1595,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 			Expect(12);
 			lhsExpr = new NAryExpr(x, new FunctionCall(new IdentifierExpr(id, id.val)), ids.Select(id => new IdentifierExpr(id, id.val)).ToList<Expr>());
 			
-			Expect(63);
+			Expect(62);
 			x = t; /* use location of := */ 
 			while (la.kind == 26) {
 				Attribute(ref kv);
@@ -1631,7 +1607,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 		} else if (StartOf(20)) {
 			lhss = new List<AssignLhs/*!*/>(); 
 			lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 
-			while (la.kind == 19 || la.kind == 64) {
+			while (la.kind == 19 || la.kind == 63) {
 				if (la.kind == 19) {
 					MapAssignIndex(out y, out indexes);
 					lhs = new MapAssignLhs(y, lhs, indexes); 
@@ -1645,7 +1621,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 				Get();
 				Ident(out id);
 				lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); 
-				while (la.kind == 19 || la.kind == 64) {
+				while (la.kind == 19 || la.kind == 63) {
 					if (la.kind == 19) {
 						MapAssignIndex(out y, out indexes);
 						lhs = new MapAssignLhs(y, lhs, indexes); 
@@ -1656,7 +1632,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 				}
 				lhss.Add(lhs); 
 			}
-			Expect(63);
+			Expect(62);
 			x = t; /* use location of := */ 
 			while (la.kind == 26) {
 				Attribute(ref kv);
@@ -1671,7 +1647,7 @@ void LabelOrAssign(out Cmd c, out IToken label) {
 			}
 			Expect(10);
 			c = new AssignCmd(x, lhss, rhss, kv); 
-		} else SynErr(145);
+		} else SynErr(144);
 	}
 
 	void ParCallCmd(out Cmd d) {
@@ -1680,11 +1656,11 @@ void ParCallCmd(out Cmd d) {
 		Cmd c = null;
 		List<CallCmd> callCmds = new List<CallCmd>();
 		
-		Expect(66);
+		Expect(65);
 		x = t; 
 		CallParams(false, false, x, out c);
 		callCmds.Add((CallCmd)c); 
-		while (la.kind == 67) {
+		while (la.kind == 66) {
 			Get();
 			CallParams(false, false, x, out c);
 			callCmds.Add((CallCmd)c); 
@@ -1713,7 +1689,7 @@ void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
 
 	void FieldAccess(out IToken x, out FieldAccess fieldAccess) {
 		Contract.Ensures(Contract.ValueAtReturn(out fieldAccess) != null); IToken id; 
-		Expect(64);
+		Expect(63);
 		x = t; 
 		Ident(out id);
 		fieldAccess = new FieldAccess(id, id.val); 
@@ -1745,7 +1721,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 			}
 			Expect(12);
 			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; 
-		} else if (la.kind == 14 || la.kind == 63) {
+		} else if (la.kind == 14 || la.kind == 62) {
 			ids.Add(new IdentifierExpr(first, first.val)); 
 			if (la.kind == 14) {
 				Get();
@@ -1757,7 +1733,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 					ids.Add(new IdentifierExpr(p, p.val)); 
 				}
 			}
-			Expect(63);
+			Expect(62);
 			Ident(out first);
 			Expect(11);
 			if (StartOf(19)) {
@@ -1771,7 +1747,7 @@ void CallParams(bool isAsync, bool isFree, IToken x, out Cmd c) {
 			}
 			Expect(12);
 			c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree; ((CallCmd) c).IsAsync = isAsync; 
-		} else SynErr(146);
+		} else SynErr(145);
 	}
 
 	void Expressions(out List<Expr>/*!*/ es) {
@@ -1789,7 +1765,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		LogicalExpression(out e0);
 		if (StartOf(21)) {
-			if (la.kind == 70 || la.kind == 71) {
+			if (la.kind == 69 || la.kind == 70) {
 				ImpliesOp();
 				x = t; 
 				ImpliesExpression(true, out e1);
@@ -1801,7 +1777,7 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
 				x = t; 
 				LogicalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); 
-				while (la.kind == 72 || la.kind == 73) {
+				while (la.kind == 71 || la.kind == 72) {
 					ExpliesOp();
 					x = t; 
 					LogicalExpression(out e1);
@@ -1812,23 +1788,23 @@ void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
 	}
 
 	void EquivOp() {
-		if (la.kind == 68) {
+		if (la.kind == 67) {
 			Get();
-		} else if (la.kind == 69) {
+		} else if (la.kind == 68) {
 			Get();
-		} else SynErr(147);
+		} else SynErr(146);
 	}
 
 	void LogicalExpression(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		RelationalExpression(out e0);
 		if (StartOf(22)) {
-			if (la.kind == 74 || la.kind == 75) {
+			if (la.kind == 73 || la.kind == 74) {
 				AndOp();
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); 
-				while (la.kind == 74 || la.kind == 75) {
+				while (la.kind == 73 || la.kind == 74) {
 					AndOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1839,7 +1815,7 @@ void LogicalExpression(out Expr/*!*/ e0) {
 				x = t; 
 				RelationalExpression(out e1);
 				e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); 
-				while (la.kind == 76 || la.kind == 77) {
+				while (la.kind == 75 || la.kind == 76) {
 					OrOp();
 					x = t; 
 					RelationalExpression(out e1);
@@ -1850,19 +1826,19 @@ void LogicalExpression(out Expr/*!*/ e0) {
 	}
 
 	void ImpliesOp() {
-		if (la.kind == 70) {
+		if (la.kind == 69) {
 			Get();
-		} else if (la.kind == 71) {
+		} else if (la.kind == 70) {
 			Get();
-		} else SynErr(148);
+		} else SynErr(147);
 	}
 
 	void ExpliesOp() {
-		if (la.kind == 72) {
+		if (la.kind == 71) {
 			Get();
-		} else if (la.kind == 73) {
+		} else if (la.kind == 72) {
 			Get();
-		} else SynErr(149);
+		} else SynErr(148);
 	}
 
 	void RelationalExpression(out Expr/*!*/ e0) {
@@ -1876,25 +1852,25 @@ void RelationalExpression(out Expr/*!*/ e0) {
 	}
 
 	void AndOp() {
-		if (la.kind == 74) {
+		if (la.kind == 73) {
 			Get();
-		} else if (la.kind == 75) {
+		} else if (la.kind == 74) {
 			Get();
-		} else SynErr(150);
+		} else SynErr(149);
 	}
 
 	void OrOp() {
-		if (la.kind == 76) {
+		if (la.kind == 75) {
 			Get();
-		} else if (la.kind == 77) {
+		} else if (la.kind == 76) {
 			Get();
-		} else SynErr(151);
+		} else SynErr(150);
 	}
 
 	void BvTerm(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		Term(out e0);
-		while (la.kind == 85) {
+		while (la.kind == 84) {
 			Get();
 			x = t; 
 			Term(out e1);
@@ -1905,7 +1881,7 @@ void BvTerm(out Expr/*!*/ e0) {
 	void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
 		switch (la.kind) {
-		case 78: {
+		case 77: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Eq; 
 			break;
@@ -1920,44 +1896,44 @@ void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 			x = t; op=BinaryOperator.Opcode.Gt; 
 			break;
 		}
-		case 79: {
+		case 78: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Le; 
 			break;
 		}
-		case 80: {
+		case 79: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Ge; 
 			break;
 		}
-		case 81: {
+		case 80: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Neq; 
 			break;
 		}
-		case 82: {
+		case 81: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Neq; 
 			break;
 		}
-		case 83: {
+		case 82: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Le; 
 			break;
 		}
-		case 84: {
+		case 83: {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Ge; 
 			break;
 		}
-		default: SynErr(152); break;
+		default: SynErr(151); break;
 		}
 	}
 
 	void Term(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; 
 		Factor(out e0);
-		while (la.kind == 86 || la.kind == 87) {
+		while (la.kind == 85 || la.kind == 86) {
 			AddOp(out x, out op);
 			Factor(out e1);
 			e0 = Expr.Binary(x, op, e0, e1); 
@@ -1976,19 +1952,19 @@ void Factor(out Expr/*!*/ e0) {
 
 	void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 86) {
+		if (la.kind == 85) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Add; 
-		} else if (la.kind == 87) {
+		} else if (la.kind == 86) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Sub; 
-		} else SynErr(153);
+		} else SynErr(152);
 	}
 
 	void Power(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; 
 		IsConstructor(out e0);
-		if (la.kind == 91) {
+		if (la.kind == 90) {
 			Get();
 			x = t; 
 			Power(out e1);
@@ -1998,25 +1974,25 @@ void Power(out Expr/*!*/ e0) {
 
 	void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
 		Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; 
-		if (la.kind == 58) {
+		if (la.kind == 57) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Mul; 
-		} else if (la.kind == 88) {
+		} else if (la.kind == 87) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Div; 
-		} else if (la.kind == 89) {
+		} else if (la.kind == 88) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.Mod; 
-		} else if (la.kind == 90) {
+		} else if (la.kind == 89) {
 			Get();
 			x = t; op=BinaryOperator.Opcode.RealDiv; 
-		} else SynErr(154);
+		} else SynErr(153);
 	}
 
 	void IsConstructor(out Expr/*!*/ e0) {
 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x, id; 
 		UnaryExpression(out e0);
-		if (la.kind == 92) {
+		if (la.kind == 91) {
 			Get();
 			x = t; 
 			Ident(out id);
@@ -2030,27 +2006,27 @@ void UnaryExpression(out Expr/*!*/ e) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
 		e = dummyExpr;
 		
-		if (la.kind == 87) {
+		if (la.kind == 86) {
 			Get();
 			x = t; 
 			UnaryExpression(out e);
 			e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); 
-		} else if (la.kind == 93 || la.kind == 94) {
+		} else if (la.kind == 92 || la.kind == 93) {
 			NegOp();
 			x = t; 
 			UnaryExpression(out e);
 			e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); 
 		} else if (StartOf(25)) {
 			CoercionExpression(out e);
-		} else SynErr(155);
+		} else SynErr(154);
 	}
 
 	void NegOp() {
-		if (la.kind == 93) {
+		if (la.kind == 92) {
 			Get();
-		} else if (la.kind == 94) {
+		} else if (la.kind == 93) {
 			Get();
-		} else SynErr(156);
+		} else SynErr(155);
 	}
 
 	void CoercionExpression(out Expr/*!*/ e) {
@@ -2074,7 +2050,7 @@ void CoercionExpression(out Expr/*!*/ e) {
 				 e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
 				}
 				
-			} else SynErr(157);
+			} else SynErr(156);
 		}
 	}
 
@@ -2086,7 +2062,7 @@ void ArrayExpression(out Expr/*!*/ e) {
 		List<Expr>/*!*/ allArgs = dummyExprSeq;
 		
 		AtomExpression(out e);
-		while (la.kind == 19 || la.kind == 64) {
+		while (la.kind == 19 || la.kind == 63) {
 			if (la.kind == 19) {
 				Get();
 				x = t; allArgs = new List<Expr> ();
@@ -2108,7 +2084,7 @@ void ArrayExpression(out Expr/*!*/ e) {
 							allArgs.Add(e1);
 							
 						}
-						if (la.kind == 63) {
+						if (la.kind == 62) {
 							Get();
 							Expression(out e1);
 							if (bvExtract || e1 is BvBounds)
@@ -2141,12 +2117,12 @@ void ArrayExpression(out Expr/*!*/ e) {
 				} else if (la.kind == 11) {
 					Get();
 					Ident(out id);
-					Expect(63);
+					Expect(62);
 					x = t; 
 					Expression(out e1);
 					Expect(12);
 					e = new NAryExpr(x, new FieldUpdate(id, id.val), new List<Expr> { e, e1 }); 
-				} else SynErr(158);
+				} else SynErr(157);
 			}
 		}
 	}
@@ -2173,18 +2149,18 @@ void AtomExpression(out Expr/*!*/ e) {
 		List<Block/*!*/>/*!*/ blocks;
 		
 		switch (la.kind) {
-		case 95: {
+		case 94: {
 			Get();
 			e = new LiteralExpr(t, false); 
 			break;
 		}
-		case 96: {
+		case 95: {
 			Get();
 			e = new LiteralExpr(t, true); 
 			break;
 		}
-		case 97: case 98: {
-			if (la.kind == 97) {
+		case 96: case 97: {
+			if (la.kind == 96) {
 				Get();
 			} else {
 				Get();
@@ -2192,8 +2168,8 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, RoundingMode.RNE); 
 			break;
 		}
-		case 99: case 100: {
-			if (la.kind == 99) {
+		case 98: case 99: {
+			if (la.kind == 98) {
 				Get();
 			} else {
 				Get();
@@ -2201,8 +2177,8 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, RoundingMode.RNA); 
 			break;
 		}
-		case 101: case 102: {
-			if (la.kind == 101) {
+		case 100: case 101: {
+			if (la.kind == 100) {
 				Get();
 			} else {
 				Get();
@@ -2210,8 +2186,8 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, RoundingMode.RTP); 
 			break;
 		}
-		case 103: case 104: {
-			if (la.kind == 103) {
+		case 102: case 103: {
+			if (la.kind == 102) {
 				Get();
 			} else {
 				Get();
@@ -2219,8 +2195,8 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, RoundingMode.RTN); 
 			break;
 		}
-		case 105: case 106: {
-			if (la.kind == 105) {
+		case 104: case 105: {
+			if (la.kind == 104) {
 				Get();
 			} else {
 				Get();
@@ -2253,7 +2229,7 @@ void AtomExpression(out Expr/*!*/ e) {
 			e = new LiteralExpr(t, t.val.Trim('"')); 
 			break;
 		}
-		case 1: case 42: case 43: case 44: case 45: {
+		case 1: case 41: case 42: case 43: case 44: {
 			Ident(out x);
 			id = new IdentifierExpr(x, x.val);  e = id; 
 			if (la.kind == 11) {
@@ -2263,12 +2239,12 @@ void AtomExpression(out Expr/*!*/ e) {
 					e = new NAryExpr(x, new FunctionCall(id), es); 
 				} else if (la.kind == 12) {
 					e = new NAryExpr(x, new FunctionCall(id), new List<Expr>()); 
-				} else SynErr(159);
+				} else SynErr(158);
 				Expect(12);
 			}
 			break;
 		}
-		case 107: {
+		case 106: {
 			Get();
 			x = t; 
 			Expect(11);
@@ -2301,19 +2277,19 @@ void AtomExpression(out Expr/*!*/ e) {
 				Expression(out e);
 				if (e is BvBounds)
 				 this.SemErr("parentheses around bitvector bounds are not allowed"); 
-			} else if (la.kind == 111 || la.kind == 112) {
+			} else if (la.kind == 110 || la.kind == 111) {
 				Forall();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
 				if (typeParams.Count + ds.Count > 0)
 				 e = new ForallExpr(x, typeParams, ds, kv, trig, e); 
-			} else if (la.kind == 113 || la.kind == 114) {
+			} else if (la.kind == 112 || la.kind == 113) {
 				Exists();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
 				if (typeParams.Count + ds.Count > 0)
 				 e = new ExistsExpr(x, typeParams, ds, kv, trig, e); 
-			} else if (la.kind == 115 || la.kind == 116) {
+			} else if (la.kind == 114 || la.kind == 115) {
 				Lambda();
 				x = t; 
 				QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
@@ -2323,20 +2299,20 @@ void AtomExpression(out Expr/*!*/ e) {
 				 e = new LambdaExpr(x, typeParams, ds, kv, e); 
 			} else if (la.kind == 9) {
 				LetExpr(out e);
-			} else SynErr(160);
+			} else SynErr(159);
 			Expect(12);
 			break;
 		}
-		case 55: {
+		case 54: {
 			IfThenElseExpression(out e);
 			break;
 		}
-		case 108: {
+		case 107: {
 			CodeExpression(out locals, out blocks);
 			e = new CodeExpr(locals, blocks); 
 			break;
 		}
-		default: SynErr(161); break;
+		default: SynErr(160); break;
 		}
 	}
 
@@ -2348,7 +2324,7 @@ void Dec(out BigDec n) {
 		} else if (la.kind == 6) {
 			Get();
 			s = t.val; 
-		} else SynErr(162);
+		} else SynErr(161);
 		try {
 		 n = BigDec.FromString(s);
 		} catch (FormatException) {
@@ -2388,11 +2364,11 @@ void BvLit(out BigNum n, out int m) {
 	}
 
 	void Forall() {
-		if (la.kind == 111) {
+		if (la.kind == 110) {
 			Get();
-		} else if (la.kind == 112) {
+		} else if (la.kind == 111) {
 			Get();
-		} else SynErr(163);
+		} else SynErr(162);
 	}
 
 	void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out List<Variable>/*!*/ ds,
@@ -2410,7 +2386,7 @@ void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out L
 			}
 		} else if (StartOf(12)) {
 			BoundVars(out ds);
-		} else SynErr(164);
+		} else SynErr(163);
 		QSep();
 		while (la.kind == 26) {
 			AttributeOrTrigger(ref kv, ref trig);
@@ -2419,19 +2395,19 @@ void QuantifierBody(IToken/*!*/ q, out List<TypeVariable>/*!*/ typeParams, out L
 	}
 
 	void Exists() {
-		if (la.kind == 113) {
+		if (la.kind == 112) {
 			Get();
-		} else if (la.kind == 114) {
+		} else if (la.kind == 113) {
 			Get();
-		} else SynErr(165);
+		} else SynErr(164);
 	}
 
 	void Lambda() {
-		if (la.kind == 115) {
+		if (la.kind == 114) {
 			Get();
-		} else if (la.kind == 116) {
+		} else if (la.kind == 115) {
 			Get();
-		} else SynErr(166);
+		} else SynErr(165);
 	}
 
 	void LetExpr(out Expr/*!*/ letexpr) {
@@ -2452,7 +2428,7 @@ void LetExpr(out Expr/*!*/ letexpr) {
 			LetVar(out v);
 			ds.Add(v); 
 		}
-		Expect(63);
+		Expect(62);
 		Expression(out e0);
 		rhss.Add(e0); 
 		while (la.kind == 14) {
@@ -2473,12 +2449,12 @@ void IfThenElseExpression(out Expr/*!*/ e) {
 		IToken/*!*/ tok;
 		Expr/*!*/ e0, e1, e2;
 		e = dummyExpr; 
-		Expect(55);
+		Expect(54);
 		tok = t; 
 		Expression(out e0);
-		Expect(110);
+		Expect(109);
 		Expression(out e1);
-		Expect(56);
+		Expect(55);
 		Expression(out e2);
 		e = new NAryExpr(tok, new IfThenElse(tok), new List<Expr>{ e0, e1, e2 }); 
 	}
@@ -2487,7 +2463,7 @@ void CodeExpression(out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ bl
 		Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new List<Variable>(); Block/*!*/ b;
 		blocks = new List<Block/*!*/>();
 		
-		Expect(108);
+		Expect(107);
 		while (la.kind == 9) {
 			LocalVars(locals);
 		}
@@ -2497,7 +2473,7 @@ void CodeExpression(out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ bl
 			SpecBlock(out b);
 			blocks.Add(b); 
 		}
-		Expect(109);
+		Expect(108);
 	}
 
 	void SpecBlock(out Block/*!*/ b) {
@@ -2521,7 +2497,7 @@ void SpecBlock(out Block/*!*/ b) {
 			}
 			
 		}
-		if (la.kind == 53) {
+		if (la.kind == 52) {
 			Get();
 			y = t; 
 			Idents(out xs);
@@ -2530,11 +2506,11 @@ void SpecBlock(out Block/*!*/ b) {
 			 ss.Add(s.val); }
 			b = new Block(x,x.val,cs,new GotoCmd(y,ss));
 			
-		} else if (la.kind == 54) {
+		} else if (la.kind == 53) {
 			Get();
 			Expression(out e);
 			b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); 
-		} else SynErr(167);
+		} else SynErr(166);
 		Expect(10);
 	}
 
@@ -2591,7 +2567,7 @@ void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
 			 trig.AddLast(new Trigger(tok, true, es, null));
 			}
 			
-		} else SynErr(168);
+		} else SynErr(167);
 		Expect(27);
 	}
 
@@ -2606,15 +2582,15 @@ void AttributeParameter(out object/*!*/ o) {
 		} else if (StartOf(19)) {
 			Expression(out e);
 			o = e; 
-		} else SynErr(169);
+		} else SynErr(168);
 	}
 
 	void QSep() {
-		if (la.kind == 117) {
+		if (la.kind == 116) {
 			Get();
-		} else if (la.kind == 118) {
+		} else if (la.kind == 117) {
 			Get();
-		} else SynErr(170);
+		} else SynErr(169);
 	}
 
 	void LetVar(out Variable/*!*/ v) {
@@ -2643,33 +2619,33 @@ public void Parse() {
 	}
 
 	static readonly bool[,]/*!*/ set = {
-		{_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,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _x,_T,_x,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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,_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,_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,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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, _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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_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,_T,_x,_x, _x,_x,_x,_T, _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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_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,_T, _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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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, _T,_T,_x,_x, _x,_x,_x,_T, _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,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _T,_T,_x,_x, _x,_x,_x,_T, _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,_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,_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,_x,_x, _x,_x,_x,_x, _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, _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,_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,_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,_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,_T, _x,_x,_x,_x, _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, _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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _x,_x,_x,_x, _T,_T,_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,_T,_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, _x,_x,_x,_x, _x,_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,_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,_T,_T, _T,_T,_x,_x, _x,_x,_x,_T, _x,_T,_T,_T, _x,_T,_x,_T, _T,_T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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, _T,_x,_x,_x, _x,_x,_T,_T, _T,_T,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_x,_x,_T, _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,_T,_T, _T,_T,_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, _x,_x,_x,_x, _x,_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,_T,_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, _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,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x},
-		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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, _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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _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,_T,_T, _T,_T,_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,_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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _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,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _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,_x,_x,_x, _x,_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}
+		{_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,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _T,_x,_T,_T, _x,_T,_x,_T, _T,_T,_x,_x, _x,_T,_T,_T, _T,_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,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _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,_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,_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,_T, _x,_x,_x,_x, _T,_T,_T,_T, _x,_T,_x,_x, _x,_x,_T,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_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,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_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,_T, _x,_x,_x,_x, _x,_x,_T,_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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_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,_T,_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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_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,_T,_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,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_x,_x, _x,_x,_T,_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,_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,_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,_x,_x,_x, _x,_x,_x,_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, _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,_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,_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,_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,_T, _x,_x,_x,_x, _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,_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,_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,_x,_x,_T, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_T,_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,_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,_x, _x,_x,_x,_x, _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,_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,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _T,_T,_T,_x, _T,_x,_T,_T, _T,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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, _T,_x,_x,_x, _x,_T,_T,_T, _T,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_x,_x,_T, _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,_T,_T,_T, _T,_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,_x, _x,_x,_x,_x, _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,_T,_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,_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, _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,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},
+		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_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, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_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,_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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _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,_T,_T,_T, _T,_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,_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,_T,_T,_T, _T,_T,_T,_T, _x,_x,_x,_T, _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,_T,_T,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_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, _x,_x,_x,_x, _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}
 
 	};
 } // end Parser
@@ -2733,138 +2709,137 @@ string GetSyntaxErrorString(int n) {
 			case 36: s = "\"async\" expected"; break;
 			case 37: s = "\"action\" expected"; break;
 			case 38: s = "\"creates\" expected"; break;
-			case 39: s = "\"using\" expected"; break;
-			case 40: s = "\"eliminates\" expected"; break;
-			case 41: s = "\"refines\" expected"; break;
-			case 42: s = "\"left\" expected"; break;
-			case 43: s = "\"right\" expected"; break;
-			case 44: s = "\"both\" expected"; break;
-			case 45: s = "\"atomic\" expected"; break;
-			case 46: s = "\"procedure\" expected"; break;
-			case 47: s = "\"requires\" expected"; break;
-			case 48: s = "\"ensures\" expected"; break;
-			case 49: s = "\"preserves\" expected"; break;
-			case 50: s = "\"implementation\" expected"; break;
-			case 51: s = "\"free\" expected"; break;
-			case 52: s = "\"modifies\" expected"; break;
-			case 53: s = "\"goto\" expected"; break;
-			case 54: s = "\"return\" expected"; break;
-			case 55: s = "\"if\" expected"; break;
-			case 56: s = "\"else\" expected"; break;
-			case 57: s = "\"while\" expected"; break;
-			case 58: s = "\"*\" expected"; break;
-			case 59: s = "\"break\" expected"; break;
-			case 60: s = "\"assert\" expected"; break;
-			case 61: s = "\"assume\" expected"; break;
-			case 62: s = "\"havoc\" expected"; break;
-			case 63: s = "\":=\" expected"; break;
-			case 64: s = "\"->\" expected"; break;
-			case 65: s = "\"call\" expected"; break;
-			case 66: s = "\"par\" expected"; break;
-			case 67: s = "\"|\" expected"; break;
-			case 68: s = "\"<==>\" expected"; break;
-			case 69: s = "\"\\u21d4\" expected"; break;
-			case 70: s = "\"==>\" expected"; break;
-			case 71: s = "\"\\u21d2\" expected"; break;
-			case 72: s = "\"<==\" expected"; break;
-			case 73: s = "\"\\u21d0\" expected"; break;
-			case 74: s = "\"&&\" expected"; break;
-			case 75: s = "\"\\u2227\" expected"; break;
-			case 76: s = "\"||\" expected"; break;
-			case 77: s = "\"\\u2228\" expected"; break;
-			case 78: s = "\"==\" expected"; break;
-			case 79: s = "\"<=\" expected"; break;
-			case 80: s = "\">=\" expected"; break;
-			case 81: s = "\"!=\" expected"; break;
-			case 82: s = "\"\\u2260\" expected"; break;
-			case 83: s = "\"\\u2264\" expected"; break;
-			case 84: s = "\"\\u2265\" expected"; break;
-			case 85: s = "\"++\" expected"; break;
-			case 86: s = "\"+\" expected"; break;
-			case 87: s = "\"-\" expected"; break;
-			case 88: s = "\"div\" expected"; break;
-			case 89: s = "\"mod\" expected"; break;
-			case 90: s = "\"/\" expected"; break;
-			case 91: s = "\"**\" expected"; break;
-			case 92: s = "\"is\" expected"; break;
-			case 93: s = "\"!\" expected"; break;
-			case 94: s = "\"\\u00ac\" expected"; break;
-			case 95: s = "\"false\" expected"; break;
-			case 96: s = "\"true\" expected"; break;
-			case 97: s = "\"roundNearestTiesToEven\" expected"; break;
-			case 98: s = "\"RNE\" expected"; break;
-			case 99: s = "\"roundNearestTiesToAway\" expected"; break;
-			case 100: s = "\"RNA\" expected"; break;
-			case 101: s = "\"roundTowardPositive\" expected"; break;
-			case 102: s = "\"RTP\" expected"; break;
-			case 103: s = "\"roundTowardNegative\" expected"; break;
-			case 104: s = "\"RTN\" expected"; break;
-			case 105: s = "\"roundTowardZero\" expected"; break;
-			case 106: s = "\"RTZ\" expected"; break;
-			case 107: s = "\"old\" expected"; break;
-			case 108: s = "\"|{\" expected"; break;
-			case 109: s = "\"}|\" expected"; break;
-			case 110: s = "\"then\" expected"; break;
-			case 111: s = "\"forall\" expected"; break;
-			case 112: s = "\"\\u2200\" expected"; break;
-			case 113: s = "\"exists\" expected"; break;
-			case 114: s = "\"\\u2203\" expected"; break;
-			case 115: s = "\"lambda\" expected"; break;
-			case 116: s = "\"\\u03bb\" expected"; break;
-			case 117: s = "\"::\" expected"; break;
-			case 118: s = "\"\\u2022\" expected"; break;
-			case 119: s = "??? expected"; break;
+			case 39: s = "\"refines\" expected"; break;
+			case 40: s = "\"using\" expected"; break;
+			case 41: s = "\"left\" expected"; break;
+			case 42: s = "\"right\" expected"; break;
+			case 43: s = "\"both\" expected"; break;
+			case 44: s = "\"atomic\" expected"; break;
+			case 45: s = "\"procedure\" expected"; break;
+			case 46: s = "\"requires\" expected"; break;
+			case 47: s = "\"ensures\" expected"; break;
+			case 48: s = "\"preserves\" expected"; break;
+			case 49: s = "\"implementation\" expected"; break;
+			case 50: s = "\"free\" expected"; break;
+			case 51: s = "\"modifies\" expected"; break;
+			case 52: s = "\"goto\" expected"; break;
+			case 53: s = "\"return\" expected"; break;
+			case 54: s = "\"if\" expected"; break;
+			case 55: s = "\"else\" expected"; break;
+			case 56: s = "\"while\" expected"; break;
+			case 57: s = "\"*\" expected"; break;
+			case 58: s = "\"break\" expected"; break;
+			case 59: s = "\"assert\" expected"; break;
+			case 60: s = "\"assume\" expected"; break;
+			case 61: s = "\"havoc\" expected"; break;
+			case 62: s = "\":=\" expected"; break;
+			case 63: s = "\"->\" expected"; break;
+			case 64: s = "\"call\" expected"; break;
+			case 65: s = "\"par\" expected"; break;
+			case 66: s = "\"|\" expected"; break;
+			case 67: s = "\"<==>\" expected"; break;
+			case 68: s = "\"\\u21d4\" expected"; break;
+			case 69: s = "\"==>\" expected"; break;
+			case 70: s = "\"\\u21d2\" expected"; break;
+			case 71: s = "\"<==\" expected"; break;
+			case 72: s = "\"\\u21d0\" expected"; break;
+			case 73: s = "\"&&\" expected"; break;
+			case 74: s = "\"\\u2227\" expected"; break;
+			case 75: s = "\"||\" expected"; break;
+			case 76: s = "\"\\u2228\" expected"; break;
+			case 77: s = "\"==\" expected"; break;
+			case 78: s = "\"<=\" expected"; break;
+			case 79: s = "\">=\" expected"; break;
+			case 80: s = "\"!=\" expected"; break;
+			case 81: s = "\"\\u2260\" expected"; break;
+			case 82: s = "\"\\u2264\" expected"; break;
+			case 83: s = "\"\\u2265\" expected"; break;
+			case 84: s = "\"++\" expected"; break;
+			case 85: s = "\"+\" expected"; break;
+			case 86: s = "\"-\" expected"; break;
+			case 87: s = "\"div\" expected"; break;
+			case 88: s = "\"mod\" expected"; break;
+			case 89: s = "\"/\" expected"; break;
+			case 90: s = "\"**\" expected"; break;
+			case 91: s = "\"is\" expected"; break;
+			case 92: s = "\"!\" expected"; break;
+			case 93: s = "\"\\u00ac\" expected"; break;
+			case 94: s = "\"false\" expected"; break;
+			case 95: s = "\"true\" expected"; break;
+			case 96: s = "\"roundNearestTiesToEven\" expected"; break;
+			case 97: s = "\"RNE\" expected"; break;
+			case 98: s = "\"roundNearestTiesToAway\" expected"; break;
+			case 99: s = "\"RNA\" expected"; break;
+			case 100: s = "\"roundTowardPositive\" expected"; break;
+			case 101: s = "\"RTP\" expected"; break;
+			case 102: s = "\"roundTowardNegative\" expected"; break;
+			case 103: s = "\"RTN\" expected"; break;
+			case 104: s = "\"roundTowardZero\" expected"; break;
+			case 105: s = "\"RTZ\" expected"; break;
+			case 106: s = "\"old\" expected"; break;
+			case 107: s = "\"|{\" expected"; break;
+			case 108: s = "\"}|\" expected"; break;
+			case 109: s = "\"then\" expected"; break;
+			case 110: s = "\"forall\" expected"; break;
+			case 111: s = "\"\\u2200\" expected"; break;
+			case 112: s = "\"exists\" expected"; break;
+			case 113: s = "\"\\u2203\" expected"; break;
+			case 114: s = "\"lambda\" expected"; break;
+			case 115: s = "\"\\u03bb\" expected"; break;
+			case 116: s = "\"::\" expected"; break;
+			case 117: s = "\"\\u2022\" expected"; break;
+			case 118: s = "??? expected"; break;
+			case 119: s = "invalid BoogiePL"; break;
 			case 120: s = "invalid BoogiePL"; break;
-			case 121: s = "invalid BoogiePL"; break;
-			case 122: s = "invalid Consts"; break;
+			case 121: s = "invalid Consts"; break;
+			case 122: s = "invalid Function"; break;
 			case 123: s = "invalid Function"; break;
-			case 124: s = "invalid Function"; break;
-			case 125: s = "invalid YieldProcedureDecl"; break;
-			case 126: s = "invalid Procedure"; break;
-			case 127: s = "invalid ActionDecl"; break;
-			case 128: s = "invalid Type"; break;
-			case 129: s = "invalid TypeAtom"; break;
-			case 130: s = "invalid Ident"; break;
-			case 131: s = "invalid TypeArgs"; break;
-			case 132: s = "invalid MoverQualifier"; break;
-			case 133: s = "invalid SpecAction"; break;
-			case 134: s = "invalid SpecYieldRequires"; break;
-			case 135: s = "invalid SpecYieldPrePost"; break;
-			case 136: s = "invalid SpecYieldEnsures"; break;
-			case 137: s = "invalid Spec"; break;
-			case 138: s = "invalid SpecPrePost"; break;
-			case 139: s = "invalid LabelOrCmd"; break;
-			case 140: s = "invalid StructuredCmd"; break;
-			case 141: s = "invalid TransferCmd"; break;
-			case 142: s = "invalid IfCmd"; break;
-			case 143: s = "invalid WhileCmd"; break;
-			case 144: s = "invalid Guard"; break;
-			case 145: s = "invalid LabelOrAssign"; break;
-			case 146: s = "invalid CallParams"; break;
-			case 147: s = "invalid EquivOp"; break;
-			case 148: s = "invalid ImpliesOp"; break;
-			case 149: s = "invalid ExpliesOp"; break;
-			case 150: s = "invalid AndOp"; break;
-			case 151: s = "invalid OrOp"; break;
-			case 152: s = "invalid RelOp"; break;
-			case 153: s = "invalid AddOp"; break;
-			case 154: s = "invalid MulOp"; break;
-			case 155: s = "invalid UnaryExpression"; break;
-			case 156: s = "invalid NegOp"; break;
-			case 157: s = "invalid CoercionExpression"; break;
-			case 158: s = "invalid ArrayExpression"; break;
+			case 124: s = "invalid YieldProcedureDecl"; break;
+			case 125: s = "invalid Procedure"; break;
+			case 126: s = "invalid ActionDecl"; break;
+			case 127: s = "invalid Type"; break;
+			case 128: s = "invalid TypeAtom"; break;
+			case 129: s = "invalid Ident"; break;
+			case 130: s = "invalid TypeArgs"; break;
+			case 131: s = "invalid MoverQualifier"; break;
+			case 132: s = "invalid SpecAction"; break;
+			case 133: s = "invalid SpecYieldRequires"; break;
+			case 134: s = "invalid SpecYieldPrePost"; break;
+			case 135: s = "invalid SpecYieldEnsures"; break;
+			case 136: s = "invalid Spec"; break;
+			case 137: s = "invalid SpecPrePost"; break;
+			case 138: s = "invalid LabelOrCmd"; break;
+			case 139: s = "invalid StructuredCmd"; break;
+			case 140: s = "invalid TransferCmd"; break;
+			case 141: s = "invalid IfCmd"; break;
+			case 142: s = "invalid WhileCmd"; break;
+			case 143: s = "invalid Guard"; break;
+			case 144: s = "invalid LabelOrAssign"; break;
+			case 145: s = "invalid CallParams"; break;
+			case 146: s = "invalid EquivOp"; break;
+			case 147: s = "invalid ImpliesOp"; break;
+			case 148: s = "invalid ExpliesOp"; break;
+			case 149: s = "invalid AndOp"; break;
+			case 150: s = "invalid OrOp"; break;
+			case 151: s = "invalid RelOp"; break;
+			case 152: s = "invalid AddOp"; break;
+			case 153: s = "invalid MulOp"; break;
+			case 154: s = "invalid UnaryExpression"; break;
+			case 155: s = "invalid NegOp"; break;
+			case 156: s = "invalid CoercionExpression"; break;
+			case 157: s = "invalid ArrayExpression"; break;
+			case 158: s = "invalid AtomExpression"; break;
 			case 159: s = "invalid AtomExpression"; break;
 			case 160: s = "invalid AtomExpression"; break;
-			case 161: s = "invalid AtomExpression"; break;
-			case 162: s = "invalid Dec"; break;
-			case 163: s = "invalid Forall"; break;
-			case 164: s = "invalid QuantifierBody"; break;
-			case 165: s = "invalid Exists"; break;
-			case 166: s = "invalid Lambda"; break;
-			case 167: s = "invalid SpecBlock"; break;
-			case 168: s = "invalid AttributeOrTrigger"; break;
-			case 169: s = "invalid AttributeParameter"; break;
-			case 170: s = "invalid QSep"; break;
+			case 161: s = "invalid Dec"; break;
+			case 162: s = "invalid Forall"; break;
+			case 163: s = "invalid QuantifierBody"; break;
+			case 164: s = "invalid Exists"; break;
+			case 165: s = "invalid Lambda"; break;
+			case 166: s = "invalid SpecBlock"; break;
+			case 167: s = "invalid AttributeOrTrigger"; break;
+			case 168: s = "invalid AttributeParameter"; break;
+			case 169: s = "invalid QSep"; break;
 
 			default: s = "error " + n; break;
 		}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 86a754aa9..2f3e7f7fb 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -220,8 +220,8 @@ public override int Read() {
 public class Scanner {
 	const char EOL = '\n';
 	const int eofSym = 0; /* pdt */
-	const int maxT = 119;
-	const int noSym = 119;
+	const int maxT = 118;
+	const int noSym = 118;
 
 
 	[ContractInvariantMethod]
@@ -532,51 +532,50 @@ void CheckLiteral() {
 			case "async": t.kind = 36; break;
 			case "action": t.kind = 37; break;
 			case "creates": t.kind = 38; break;
-			case "using": t.kind = 39; break;
-			case "eliminates": t.kind = 40; break;
-			case "refines": t.kind = 41; break;
-			case "left": t.kind = 42; break;
-			case "right": t.kind = 43; break;
-			case "both": t.kind = 44; break;
-			case "atomic": t.kind = 45; break;
-			case "procedure": t.kind = 46; break;
-			case "requires": t.kind = 47; break;
-			case "ensures": t.kind = 48; break;
-			case "preserves": t.kind = 49; break;
-			case "implementation": t.kind = 50; break;
-			case "free": t.kind = 51; break;
-			case "modifies": t.kind = 52; break;
-			case "goto": t.kind = 53; break;
-			case "return": t.kind = 54; break;
-			case "if": t.kind = 55; break;
-			case "else": t.kind = 56; break;
-			case "while": t.kind = 57; break;
-			case "break": t.kind = 59; break;
-			case "assert": t.kind = 60; break;
-			case "assume": t.kind = 61; break;
-			case "havoc": t.kind = 62; break;
-			case "call": t.kind = 65; break;
-			case "par": t.kind = 66; break;
-			case "div": t.kind = 88; break;
-			case "mod": t.kind = 89; break;
-			case "is": t.kind = 92; break;
-			case "false": t.kind = 95; break;
-			case "true": t.kind = 96; break;
-			case "roundNearestTiesToEven": t.kind = 97; break;
-			case "RNE": t.kind = 98; break;
-			case "roundNearestTiesToAway": t.kind = 99; break;
-			case "RNA": t.kind = 100; break;
-			case "roundTowardPositive": t.kind = 101; break;
-			case "RTP": t.kind = 102; break;
-			case "roundTowardNegative": t.kind = 103; break;
-			case "RTN": t.kind = 104; break;
-			case "roundTowardZero": t.kind = 105; break;
-			case "RTZ": t.kind = 106; break;
-			case "old": t.kind = 107; break;
-			case "then": t.kind = 110; break;
-			case "forall": t.kind = 111; break;
-			case "exists": t.kind = 113; break;
-			case "lambda": t.kind = 115; break;
+			case "refines": t.kind = 39; break;
+			case "using": t.kind = 40; break;
+			case "left": t.kind = 41; break;
+			case "right": t.kind = 42; break;
+			case "both": t.kind = 43; break;
+			case "atomic": t.kind = 44; break;
+			case "procedure": t.kind = 45; break;
+			case "requires": t.kind = 46; break;
+			case "ensures": t.kind = 47; break;
+			case "preserves": t.kind = 48; break;
+			case "implementation": t.kind = 49; break;
+			case "free": t.kind = 50; break;
+			case "modifies": t.kind = 51; break;
+			case "goto": t.kind = 52; break;
+			case "return": t.kind = 53; break;
+			case "if": t.kind = 54; break;
+			case "else": t.kind = 55; break;
+			case "while": t.kind = 56; break;
+			case "break": t.kind = 58; break;
+			case "assert": t.kind = 59; break;
+			case "assume": t.kind = 60; break;
+			case "havoc": t.kind = 61; break;
+			case "call": t.kind = 64; break;
+			case "par": t.kind = 65; break;
+			case "div": t.kind = 87; break;
+			case "mod": t.kind = 88; break;
+			case "is": t.kind = 91; break;
+			case "false": t.kind = 94; break;
+			case "true": t.kind = 95; break;
+			case "roundNearestTiesToEven": t.kind = 96; break;
+			case "RNE": t.kind = 97; break;
+			case "roundNearestTiesToAway": t.kind = 98; break;
+			case "RNA": t.kind = 99; break;
+			case "roundTowardPositive": t.kind = 100; break;
+			case "RTP": t.kind = 101; break;
+			case "roundTowardNegative": t.kind = 102; break;
+			case "RTN": t.kind = 103; break;
+			case "roundTowardZero": t.kind = 104; break;
+			case "RTZ": t.kind = 105; break;
+			case "old": t.kind = 106; break;
+			case "then": t.kind = 109; break;
+			case "forall": t.kind = 110; break;
+			case "exists": t.kind = 112; break;
+			case "lambda": t.kind = 114; break;
 			default: break;
 		}
 	}
@@ -860,67 +859,67 @@ void CheckLiteral() {
 			case 67:
 				{t.kind = 26; break;}
 			case 68:
-				{t.kind = 63; break;}
+				{t.kind = 62; break;}
 			case 69:
-				{t.kind = 64; break;}
+				{t.kind = 63; break;}
 			case 70:
-				{t.kind = 68; break;}
+				{t.kind = 67; break;}
 			case 71:
-				{t.kind = 69; break;}
+				{t.kind = 68; break;}
 			case 72:
-				{t.kind = 70; break;}
+				{t.kind = 69; break;}
 			case 73:
-				{t.kind = 71; break;}
+				{t.kind = 70; break;}
 			case 74:
-				{t.kind = 73; break;}
+				{t.kind = 72; break;}
 			case 75:
 				if (ch == '&') {AddCh(); goto case 76;}
 				else {goto case 0;}
 			case 76:
-				{t.kind = 74; break;}
+				{t.kind = 73; break;}
 			case 77:
-				{t.kind = 75; break;}
+				{t.kind = 74; break;}
 			case 78:
-				{t.kind = 76; break;}
+				{t.kind = 75; break;}
 			case 79:
-				{t.kind = 77; break;}
+				{t.kind = 76; break;}
 			case 80:
-				{t.kind = 80; break;}
+				{t.kind = 79; break;}
 			case 81:
-				{t.kind = 81; break;}
+				{t.kind = 80; break;}
 			case 82:
-				{t.kind = 82; break;}
+				{t.kind = 81; break;}
 			case 83:
-				{t.kind = 83; break;}
+				{t.kind = 82; break;}
 			case 84:
-				{t.kind = 84; break;}
+				{t.kind = 83; break;}
 			case 85:
-				{t.kind = 85; break;}
+				{t.kind = 84; break;}
 			case 86:
-				{t.kind = 90; break;}
+				{t.kind = 89; break;}
 			case 87:
-				{t.kind = 91; break;}
+				{t.kind = 90; break;}
 			case 88:
-				{t.kind = 94; break;}
+				{t.kind = 93; break;}
 			case 89:
-				{t.kind = 108; break;}
+				{t.kind = 107; break;}
 			case 90:
-				{t.kind = 109; break;}
+				{t.kind = 108; break;}
 			case 91:
-				{t.kind = 112; break;}
+				{t.kind = 111; break;}
 			case 92:
-				{t.kind = 114; break;}
+				{t.kind = 113; break;}
 			case 93:
-				{t.kind = 116; break;}
+				{t.kind = 115; break;}
 			case 94:
-				{t.kind = 117; break;}
+				{t.kind = 116; break;}
 			case 95:
-				{t.kind = 118; break;}
+				{t.kind = 117; break;}
 			case 96:
-				recEnd = pos; recKind = 87;
+				recEnd = pos; recKind = 86;
 				if (ch == '0') {AddCh(); goto case 16;}
 				else if (ch == '>') {AddCh(); goto case 69;}
-				else {t.kind = 87; break;}
+				else {t.kind = 86; break;}
 			case 97:
 				recEnd = pos; recKind = 13;
 				if (ch == '=') {AddCh(); goto case 68;}
@@ -943,34 +942,34 @@ void CheckLiteral() {
 				if (ch == '=') {AddCh(); goto case 107;}
 				else {t.kind = 32; break;}
 			case 102:
-				recEnd = pos; recKind = 58;
+				recEnd = pos; recKind = 57;
 				if (ch == '*') {AddCh(); goto case 87;}
-				else {t.kind = 58; break;}
+				else {t.kind = 57; break;}
 			case 103:
-				recEnd = pos; recKind = 67;
+				recEnd = pos; recKind = 66;
 				if (ch == '|') {AddCh(); goto case 78;}
 				else if (ch == '{') {AddCh(); goto case 89;}
-				else {t.kind = 67; break;}
+				else {t.kind = 66; break;}
 			case 104:
-				recEnd = pos; recKind = 93;
+				recEnd = pos; recKind = 92;
 				if (ch == '=') {AddCh(); goto case 81;}
-				else {t.kind = 93; break;}
+				else {t.kind = 92; break;}
 			case 105:
-				recEnd = pos; recKind = 86;
+				recEnd = pos; recKind = 85;
 				if (ch == '+') {AddCh(); goto case 85;}
-				else {t.kind = 86; break;}
+				else {t.kind = 85; break;}
 			case 106:
-				recEnd = pos; recKind = 79;
+				recEnd = pos; recKind = 78;
 				if (ch == '=') {AddCh(); goto case 108;}
-				else {t.kind = 79; break;}
+				else {t.kind = 78; break;}
 			case 107:
-				recEnd = pos; recKind = 78;
+				recEnd = pos; recKind = 77;
 				if (ch == '>') {AddCh(); goto case 72;}
-				else {t.kind = 78; break;}
+				else {t.kind = 77; break;}
 			case 108:
-				recEnd = pos; recKind = 72;
+				recEnd = pos; recKind = 71;
 				if (ch == '>') {AddCh(); goto case 70;}
-				else {t.kind = 72; break;}
+				else {t.kind = 71; break;}
 
 		}
 		t.val = new String(tval, 0, tlen);
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index da23643fa..8540302e5 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -647,22 +647,6 @@ public virtual ActionDeclRef VisitActionDeclRef(ActionDeclRef node)
       return node;
     }
 
-    public virtual ElimDecl VisitElimDecl(ElimDecl node)
-    {
-      node.Abstraction = VisitActionDeclRef(node.Abstraction);
-      node.Target = VisitActionDeclRef(node.Target);
-      return node;
-    }
-
-    public virtual List<ElimDecl> VisitElimDeclSeq(List<ElimDecl> node)
-    {
-      for (int i = 0; i < node.Count; i++)
-      {
-        node[i] = VisitElimDecl(node[i]);
-      }
-      return node;
-    }
-
     public virtual Procedure VisitActionDecl(ActionDecl node)
     {
       for (int i = 0; i < node.Creates.Count; i++)
@@ -677,7 +661,6 @@ public virtual Procedure VisitActionDecl(ActionDecl node)
       {
         node.InvariantAction = VisitActionDeclRef(node.InvariantAction);
       }
-      node.Eliminates = VisitElimDeclSeq(node.Eliminates);
       node.YieldRequires = VisitCallCmdSeq(node.YieldRequires);
       return VisitProcedure(node);
     }
diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
index bd9712afb..d3e91542e 100644
--- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs
+++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
@@ -667,16 +667,6 @@ public override ActionDeclRef VisitActionDeclRef(ActionDeclRef node)
     throw new LeanConversionException(node.tok, $"Unsupported: ActionDeclRef ({node}).");
   }
 
-  public override ElimDecl VisitElimDecl(ElimDecl node)
-  {
-    throw new LeanConversionException(node.tok, $"Unsupported: ElimDecl ({node}).");
-  }
-
-  public override List<ElimDecl> VisitElimDeclSeq(List<ElimDecl> node)
-  {
-    throw new LeanConversionException(Token.NoToken, $"Unsupported: List<ElimDecl> ({node}).");
-  }
-
   public override Axiom VisitAxiom(Axiom node)
   {
     // This will take two more steps: