5 files changed, 11 insertions, 11 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index c9545c93..fd445bc0 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -58,7 +58,7 @@ module CoRecursion {
   }
 }
 
-ghost module S {
+abstract module S {
   class C {
     var f: int;
     method m()
@@ -91,7 +91,7 @@ method NotMain() {
 }
 
 
-ghost module S1 {
+abstract module S1 {
   import B as S default T;
   static method do()
 }
diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy
index dbf39106..e4bd4605 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy
+++ b/Test/dafny0/RefinementModificationChecking.dfy
@@ -1,5 +1,5 @@
 
-ghost module R1 {
+abstract module R1 {
   var f: int;
   method m(y: set<int>) returns (r: int)
     modifies this;
@@ -8,7 +8,7 @@ ghost module R1 {
   }
 }
 
-ghost module R2 refines R1 {
+abstract module R2 refines R1 {
   var g: nat;
   method m ...
   {
diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 094e7be7..63c55506 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -4,7 +4,7 @@
 // Version with proof divided into stages:  June 2012.
 // Copyright (c) 2008-2012 Microsoft.
 
-ghost module M0 {
+abstract module M0 {
   // In this module, we declare the Node class, the definition of Reachability, and the specification
   // and implementation of the Schorr-Waite algorithm.
 
@@ -140,7 +140,7 @@ ghost module M0 {
   }
 }
 
-ghost module M1 refines M0 {
+abstract module M1 refines M0 {
   // In this superposition, we start reasoning about the marks.  In particular, we prove that the method
   // marks all reachable nodes.
   method SchorrWaite...
@@ -176,7 +176,7 @@ ghost module M1 refines M0 {
   }
 }
 
-ghost module M2 refines M1 {
+abstract module M2 refines M1 {
   // In this superposition, we prove that only reachable nodes are marked.  Essentially, we want
   // to add a loop invariant that says t is reachable from root, because then the loop invariant
   // that marked nodes are reachable follows.  More precisely, we need to say that the node
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index d8938aa7..93bf1812 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -1,4 +1,4 @@
-ghost module A {
+abstract module A {
   import L = Library;
   class {:autocontracts} StoreAndRetrieve<Thing> {
     ghost var Contents: set<Thing>;
diff --git a/Test/dafny3/CachedContainer.dfy b/Test/dafny3/CachedContainer.dfy
index 9bde80da..6ac5ff2f 100644
--- a/Test/dafny3/CachedContainer.dfy
+++ b/Test/dafny3/CachedContainer.dfy
@@ -1,5 +1,5 @@
-// give the method signatures and specs 
-ghost module M0 {
+// give the method signatures and specs
+abstract module M0 {
   class {:autocontracts} Container<T(==)> {
     ghost var Contents: set<T>;
     predicate Valid()
@@ -16,7 +16,7 @@ ghost module M0 {
 }
 
 // provide bodies for the methods
-ghost module M1 refines M0 {
+abstract module M1 refines M0 {
   class Container<T(==)> {
     constructor... {
       Contents := {};