Eliminate redundant checks of newtype and opaque function well-formedness from included files

1 files changed, 1 insertions, 1 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index 4cda8fd8..091ee24a 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -492,7 +492,7 @@ namespace Microsoft.Dafny
             newToken._val = fWithBody.Name;

             newToken._kind = f.tok.kind;

             newToken._pos = f.tok.pos;

-            fWithBody.tok = newToken;

+            fWithBody.tok = (f.tok is IncludeToken) ? new IncludeToken(newToken) : (Boogie.IToken)newToken;

 

             // Annotate the new function so we remember that we introduced it

             fWithBody.Attributes = new Attributes("opaque_full", new List<Expression>(), fWithBody.Attributes);