From d9f2a82a417703f3669ba8399dcc8bcf34c3d742 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 26 May 2011 00:02:57 -0700
Subject: Dafny: retired the "call" keyword

---
 Test/dafny1/UltraFilter.dfy | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Test/dafny1/UltraFilter.dfy')

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 61e86836..189ff2b5 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -22,9 +22,9 @@ class UltraFilter<G> {
   {
     if (M !in f) {
       // instantiate 'g' with the following 'h'
-      call h := H(f, S, M);
-      call Lemma_HIsFilter(h, f, S, M);
-      call Lemma_FHOrdering0(h, f, S, M);
+      var h := H(f, S, M);
+      Lemma_HIsFilter(h, f, S, M);
+      Lemma_FHOrdering0(h, f, S, M);
     }
   }
 
@@ -44,9 +44,9 @@ class UltraFilter<G> {
     // call Lemma_H1(h, f, S, M, *, *);
     assume (forall C, D :: C in h && D in h ==> C * D in h);
 
-    call Lemma_H2(h, f, S, M);
+    Lemma_H2(h, f, S, M);
 
-    call Lemma_H3(h, f, S, M);
+    Lemma_H3(h, f, S, M);
   }
 
   method Lemma_H0(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>, A: set<G>, B: set<G>)
-- 
cgit v1.2.3