1 files changed, 19 insertions, 15 deletions
diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy
index 70d0b989..052918d0 100644
--- a/Test/dafny0/RefinementModificationChecking.dfy
+++ b/Test/dafny0/RefinementModificationChecking.dfy
@@ -2,25 +2,29 @@
 // RUN: %diff "%s.expect" "%t"
 
 abstract module R1 {
-  var f: int;
-  method m(y: set<int>) returns (r: int)
-    modifies this;
-  {
-    var t := y;
+  class HappyBay {
+    var f: int;
+    method m(y: set<int>) returns (r: int)
+      modifies this;
+    {
+      var t := y;
+    }
   }
 }
 
 module R2 refines R1 {
-  var g: nat;
-  method m ...
-  {
-    ...;
-    var x := 3;
-    t := {1}; // error: previous local
-    r := 3; // error: out parameter
-    f := 4; // error: previously defined field
-    x := 6; // fine: new local
-    g := 34;// fine: new field
+  class HappyBay {
+    var g: nat;
+    method m ...
+    {
+      ...;
+      var x := 3;
+      t := {1}; // error: previous local
+      r := 3; // error: out parameter
+      f := 4; // error: previously defined field
+      x := 6; // fine: new local
+      g := 34;// fine: new field
+    }
   }
 }