Dafny: fixed bug in which _module scope declarations were not verified.

1 files changed, 6 insertions, 1 deletions

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 931970ca..77e4d2ef 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -214,12 +214,17 @@ bool IsAttribute() {
 				ClassMemberDecl(membersDefaultClass, isGhost, false);

 			} else SynErr(108);

 		}

+		DefaultClassDecl defaultClass = null;

 		foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

-		 DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

+		 defaultClass = topleveldecl as DefaultClassDecl;

 		 if (defaultClass != null) {

 		   defaultClass.Members.AddRange(membersDefaultClass);

 		   break;

 		 }

+		}

+		if (defaultClass == null) { // create the default class here, because it wasn't found

+      defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);

+		  defaultModule.TopLevelDecls.Add(defaultClass);

 		} 

 		Expect(0);

 	}