1 files changed, 9 insertions, 11 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index faf79a30..598b53da 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -166,12 +166,12 @@ namespace Microsoft.Dafny {
         };
         var readsFrame = new List<FrameExpression> { new FrameExpression(tok, readsIS, null) };
         var req = new Function(tok, "requires", false, true,
-          new List<TypeParameter>(), tok, args, Type.Bool,
+          new List<TypeParameter>(), args, Type.Bool,
           new List<Expression>(), readsFrame, new List<Expression>(),
           new Specification<Expression>(new List<Expression>(), null),
           null, new Attributes("axiom", new List<Attributes.Argument>(), null), null);
         var reads = new Function(tok, "reads", false, true,
-          new List<TypeParameter>(), tok, args, new SetType(new ObjectType()),
+          new List<TypeParameter>(), args, new SetType(new ObjectType()),
           new List<Expression>(), readsFrame, new List<Expression>(),
           new Specification<Expression>(new List<Expression>(), null),
           null, new Attributes("axiom", new List<Attributes.Argument>(), null), null);
@@ -2645,7 +2645,6 @@ namespace Microsoft.Dafny {
   public class Function : MemberDecl, TypeParameter.ParentType, ICallable {
     public bool IsRecursive;  // filled in during resolution
     public readonly List<TypeParameter> TypeArgs;
-    public readonly IToken OpenParen;  // can be null (for predicates), if there are no formals
     public readonly List<Formal> Formals;
     public readonly Type ResultType;
     public readonly List<Expression> Req;
@@ -2700,7 +2699,7 @@ namespace Microsoft.Dafny {
     /// Note, functions are "ghost" by default; a non-ghost function is called a "function method".
     /// </summary>
     public Function(IToken tok, string name, bool isStatic, bool isGhost,
-                    List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals, Type resultType,
+                    List<TypeParameter> typeArgs, List<Formal> formals, Type resultType,
                     List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
                     Expression body, Attributes attributes, IToken signatureEllipsis)
       : base(tok, name, isStatic, isGhost, attributes) {
@@ -2715,7 +2714,6 @@ namespace Microsoft.Dafny {
       Contract.Requires(cce.NonNullElements(ens));
       Contract.Requires(decreases != null);
       this.TypeArgs = typeArgs;
-      this.OpenParen = openParen;
       this.Formals = formals;
       this.ResultType = resultType;
       this.Req = req;
@@ -2751,10 +2749,10 @@ namespace Microsoft.Dafny {
     }
     public readonly BodyOriginKind BodyOrigin;
     public Predicate(IToken tok, string name, bool isStatic, bool isGhost,
-                     List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,
+                     List<TypeParameter> typeArgs, List<Formal> formals,
                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
                      Expression body, BodyOriginKind bodyOrigin, Attributes attributes, IToken signatureEllipsis)
-      : base(tok, name, isStatic, isGhost, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureEllipsis) {
+      : base(tok, name, isStatic, isGhost, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureEllipsis) {
       Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null);
       BodyOrigin = bodyOrigin;
     }
@@ -2768,10 +2766,10 @@ namespace Microsoft.Dafny {
     public readonly Formal K;
     public readonly CoPredicate Co;
     public PrefixPredicate(IToken tok, string name, bool isStatic,
-                     List<TypeParameter> typeArgs, IToken openParen, Formal k, List<Formal> formals,
+                     List<TypeParameter> typeArgs, Formal k, List<Formal> formals,
                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
                      Expression body, Attributes attributes, CoPredicate coPred)
-      : base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null) {
+      : base(tok, name, isStatic, true, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null) {
       Contract.Requires(k != null);
       Contract.Requires(coPred != null);
       Contract.Requires(formals != null && 1 <= formals.Count && formals[0] == k);
@@ -2786,10 +2784,10 @@ namespace Microsoft.Dafny {
     public PrefixPredicate PrefixPredicate;  // filled in during resolution (name registration)
 
     public CoPredicate(IToken tok, string name, bool isStatic,
-                     List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,
+                     List<TypeParameter> typeArgs, List<Formal> formals,
                      List<Expression> req, List<FrameExpression> reads, List<Expression> ens,
                      Expression body, Attributes attributes, IToken signatureEllipsis)
-      : base(tok, name, isStatic, true, typeArgs, openParen, formals, new BoolType(),
+      : base(tok, name, isStatic, true, typeArgs, formals, new BoolType(),
              req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, attributes, signatureEllipsis) {
     }