1 files changed, 17 insertions, 17 deletions
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index 59052ac2..01e14585 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -38,17 +38,17 @@ module J imports G, M {
 module X2 imports X1 {
   class MyClass2 {
     method Down(x1: MyClass1, x0: MyClass0) {
-      call x1.Down(x0);
+      x1.Down(x0);
     }
     method WayDown(x0: MyClass0, g: ClassG) {
-      call x0.Down();
-      call g.T();  // allowed, because this follows import relation
+      x0.Down();
+      g.T();  // allowed, because this follows import relation
       var t := g.TFunc();  // allowed, because this follows import relation
     }
     method Up() {
     }
     method Somewhere(y: MyClassY) {
-      call y.M();  // error: does not follow import relation
+      y.M();  // error: does not follow import relation
     }
   }
 }
@@ -56,10 +56,10 @@ module X2 imports X1 {
 module X1 imports X0 {
   class MyClass1 {
     method Down(x0: MyClass0) {
-      call x0.Down();
+      x0.Down();
     }
     method Up(x2: MyClass2) {
-      call x2.Up();  // error: does not follow import relation
+      x2.Up();  // error: does not follow import relation
     }
   }
 }
@@ -69,7 +69,7 @@ module X0 {
     method Down() {
     }
     method Up(x1: MyClass1, x2: MyClass2) {
-      call x1.Up(x2);  // error: does not follow import relation
+      x1.Up(x2);  // error: does not follow import relation
     }
   }
 }
@@ -78,7 +78,7 @@ module YY {
   class MyClassY {
     method M() { }
     method P(g: ClassG) {
-      call g.T();  // allowed, because this follows import relation
+      g.T();  // allowed, because this follows import relation
       var t := g.TFunc();  // allowed, because this follows import relation
     }
   }
@@ -88,20 +88,20 @@ class ClassG {
   method T() { }
   function method TFunc(): int { 10 }
   method V(y: MyClassY) {
-    call y.M();  // error: does not follow import relation
+    y.M();  // error: does not follow import relation
   }
 }
 
 method Ping() {
-  call Pong();  // allowed: intra-module call
+  Pong();  // allowed: intra-module call
 }
 
 method Pong() {
-  call Ping();  // allowed: intra-module call
+  Ping();  // allowed: intra-module call
 }
 
 method ProcG(g: ClassG) {
-  call g.T();  // allowed: intra-module call
+  g.T();  // allowed: intra-module call
   var t := g.TFunc();  // allowed: intra-module call
 }
 
@@ -111,11 +111,11 @@ class Ghosty {
   method Caller() {
     var x := 3;
     ghost var y := 3;
-    call Callee(x, y);  // fine
-    call Callee(x, x);  // fine
-    call Callee(y, x);  // error: cannot pass in ghost to a physical formal
-    call Theorem(x);  // fine
-    call Theorem(y);  // fine, because it's a ghost method
+    Callee(x, y);  // fine
+    Callee(x, x);  // fine
+    Callee(y, x);  // error: cannot pass in ghost to a physical formal
+    Theorem(x);  // fine
+    Theorem(y);  // fine, because it's a ghost method
   }
   method Callee(a: int, ghost b: int) { }
   ghost method Theorem(a: int) { }