Merge

16 files changed, 241 insertions, 263 deletions

diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy
index b4980d4b..88b06605 100644
--- a/Test/dafny1/BinaryTree.dfy
+++ b/Test/dafny1/BinaryTree.dfy
@@ -32,7 +32,7 @@ class IntSet {
     if (root == null) {

       present := false;

     } else {

-      call present := root.Find(x);

+      present := root.Find(x);

     }

   }

 

@@ -42,7 +42,7 @@ class IntSet {
     ensures Valid() && fresh(Repr - old(Repr));

     ensures Contents == old(Contents) + {x};

   { 

-    call t := InsertHelper(x, root);

+    var t := InsertHelper(x, root);

     root := t;

     Contents := root.Contents;

     Repr := root.Repr + {this};

@@ -64,12 +64,12 @@ class IntSet {
     } else {

       if (x < n.data) {

         assert n.right == null || n.right.Valid();

-        call t := InsertHelper(x, n.left);

+        var t := InsertHelper(x, n.left);

         n.left := t;

         n.Repr := n.Repr + n.left.Repr;

       } else {

         assert n.left == null || n.left.Valid();

-        call t := InsertHelper(x, n.right);

+        var t := InsertHelper(x, n.right);

         n.right := t;

         n.Repr := n.Repr + n.right.Repr;

       }

@@ -85,7 +85,7 @@ class IntSet {
     ensures Contents == old(Contents) - {x};

   {

     if (root != null) {

-      call newRoot := root.Remove(x);

+      var newRoot := root.Remove(x);

       root := newRoot;

       if (root == null) {

         Contents := {};

@@ -152,9 +152,9 @@ class Node {
     if (x == data) {

       present := true;

     } else if (left != null && x < data) {

-      call present := left.Find(x);

+      present := left.Find(x);

     } else if (right != null && data < x) {

-      call present := right.Find(x);

+      present := right.Find(x);

     } else {

       present := false;

     }

@@ -171,12 +171,12 @@ class Node {
   {

     node := this;

     if (left != null && x < data) {

-      call t := left.Remove(x);

+      var t := left.Remove(x);

       left := t;

       Contents := Contents - {x};

       if (left != null) { Repr := Repr + left.Repr; }

     } else if (right != null && data < x) {

-      call t := right.Remove(x);

+      var t := right.Remove(x);

       right := t;

       Contents := Contents - {x};

       if (right != null) { Repr := Repr + right.Repr; }

@@ -189,7 +189,7 @@ class Node {
         node := left;

       } else {

         // rotate

-        call min, r := right.RemoveMin();

+        var min, r := right.RemoveMin();

         data := min;  right := r;

         Contents := Contents - {x};

         if (right != null) { Repr := Repr + right.Repr; }

@@ -211,7 +211,8 @@ class Node {
       min := data;

       node := right;

     } else {

-      call min, t := left.RemoveMin();

+      var t;

+      min, t := left.RemoveMin();

       left := t;

       node := this;

       Contents := Contents - {min};

@@ -225,9 +226,9 @@ class Main {
   {

     var s := new IntSet.Init();

 

-    call s.Insert(12);

-    call s.Insert(24);

-    call present := s.Find(x);

+    s.Insert(12);

+    s.Insert(24);

+    var present := s.Find(x);

     assert present <==> x == 12 || x == 24;

   }

 

@@ -235,8 +236,8 @@ class Main {
     requires s != null && s.Valid();

     modifies s.Repr;

   {

-    call s.Insert(x);

-    call s.Insert(24);

+    s.Insert(x);

+    s.Insert(24);

     assert old(s.Contents) - {x,24} == s.Contents - {x,24};

   }

 }

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index 089a72c4..2dc49cd9 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -57,7 +57,7 @@ class ExtensibleArray<T> {
     if (M <= i) {

       t := elements[i - M];

     } else {

-      call arr := more.Get(i / 256);

+      var arr := more.Get(i / 256);

       t := arr[i % 256];

     }

   }

@@ -72,7 +72,7 @@ class ExtensibleArray<T> {
     if (M <= i) {

       elements[i - M] := t;

     } else {

-      call arr := more.Get(i / 256);

+      var arr := more.Get(i / 256);

       arr[i % 256] := t;

     }

     Contents := Contents[i := t];

@@ -94,7 +94,7 @@ class ExtensibleArray<T> {
         Repr := Repr + {more} + more.Repr;

       }

       // "elements" is full, so move it into "more" and allocate a new array

-      call more.Append(elements);

+      more.Append(elements);

       Repr := Repr + more.Repr;

       M := M + 256;

       elements := new T[256];

@@ -113,14 +113,14 @@ method Main() {
     invariant a.Valid() && fresh(a.Repr);

     invariant |a.Contents| == n;

   {

-    call a.Append(n);

+    a.Append(n);

     n := n + 1;

   }

-  call k := a.Get(570); print k, "\n";

-  call k := a.Get(0); print k, "\n";

-  call k := a.Get(1000); print k, "\n";

-  call a.Set(1000, 23);

-  call k := a.Get(0); print k, "\n";

-  call k := a.Get(1000); print k, "\n";

-  call k := a.Get(66000); print k, "\n";

+  var k := a.Get(570); print k, "\n";

+  k := a.Get(0); print k, "\n";

+  k := a.Get(1000); print k, "\n";

+  a.Set(1000, 23);

+  k := a.Get(0); print k, "\n";

+  k := a.Get(1000); print k, "\n";

+  k := a.Get(66000); print k, "\n";

 }

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index cff8b934..76e67205 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -9,7 +9,7 @@ method FindZero(a: array<int>) returns (r: int)
     invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;

   {

     if (a[n] == 0) { r := n; return; }

-    call Lemma(a, n, a[n]);

+    Lemma(a, n, a[n]);

     n := n + a[n];

   }

   r := -1;

@@ -25,6 +25,6 @@ ghost method Lemma(a: array<int>, k: int, m: int)
 {

   if (0 < m && k < a.Length) {

     assert a[k] != 0;

-    call Lemma(a, k+1, m-1);

+    Lemma(a, k+1, m-1);

   }

 }

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 7c7d3baf..15cc1ffe 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -24,8 +24,8 @@ class IntegerInduction {
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);

   {

     if (n != 0) {

-      call Theorem0(n-1);

-      call Lemma(n-1);

+      Theorem0(n-1);

+      Lemma(n-1);

     }

   }

 

@@ -33,7 +33,7 @@ class IntegerInduction {
     requires 0 <= n;

     ensures 2 * Gauss(n) == n*(n+1);

   {

-    if (n != 0) { call Lemma(n-1); }

+    if (n != 0) { Lemma(n-1); }

   }

 

   // Here is another proof.  It states the lemma as part of the theorem, and

@@ -45,7 +45,7 @@ class IntegerInduction {
     ensures 2 * Gauss(n) == n*(n+1);

   {

     if (n != 0) {

-      call Theorem1(n-1);

+      Theorem1(n-1);

     }

   }

 

@@ -64,7 +64,7 @@ class IntegerInduction {
     ensures SumOfCubes(n) == Gauss(n) * Gauss(n);

   {

     if (n != 0) {

-      call Theorem2(n-1);

+      Theorem2(n-1);

 

       assert (forall m :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));

     }

@@ -84,7 +84,7 @@ class IntegerInduction {
     ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);

   {

     if (n != 0) {

-      call Theorem3(n-1);

+      Theorem3(n-1);

     }

   }

 

@@ -112,7 +112,7 @@ class IntegerInduction {
     if (*) {

       assert (forall m :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));

     } else {

-      call Theorem4();

+      Theorem4();

     }

   }

 

@@ -136,10 +136,7 @@ class IntegerInduction {
   }

 }

 

-datatype Tree<T> {

-  Leaf(T);

-  Branch(Tree<T>, Tree<T>);

-}

+datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);

 

 class DatatypeInduction<T> {

   function LeafCount<T>(tree: Tree<T>): int

@@ -182,7 +179,7 @@ function FooD(n: nat, d: D): int
 {

   match d

   case Nothing =>

-    if n == 0 then 10 else FooD(n-1, #D.Something(d))

+    if n == 0 then 10 else FooD(n-1, D.Something(d))

   case Something(next) =>

     if n < 100 then n + 12 else FooD(n-13, next)

 }

diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
index 86ad451d..81b3f4c9 100644
--- a/Test/dafny1/MatrixFun.dfy
+++ b/Test/dafny1/MatrixFun.dfy
@@ -64,20 +64,20 @@ method Main()
   B[0,0] := true;  B[0,1] := false;  B[0,2] := false;  B[0,3] := true;  B[0,4] := false;

   B[1,0] := true;  B[1,1] := true;   B[1,2] := true;   B[1,3] := true;  B[1,4] := false;

   print "Before:\n";

-  call PrintMatrix(B);

-  call MirrorImage(B);

+  PrintMatrix(B);

+  MirrorImage(B);

   print "Mirror image:\n";

-  call PrintMatrix(B);

+  PrintMatrix(B);

 

   var A := new int[3,3];

   A[0,0] := 5;  A[0,1] := 7;  A[0,2] := 9;

   A[1,0] := 6;  A[1,1] := 2;  A[1,2] := 3;

   A[2,0] := 7;  A[2,1] := 1;  A[2,2] := 0;

   print "Before:\n";

-  call PrintMatrix(A);

-  call Flip(A);

+  PrintMatrix(A);

+  Flip(A);

   print "Flip:\n";

-  call PrintMatrix(A);

+  PrintMatrix(A);

 }

 

 method PrintMatrix<T>(m: array2<T>)

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index db1c60fa..6e19ab8f 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -41,7 +41,7 @@ class PriorityQueue {
   {

     n := n + 1;

     a[n] := x;

-    call SiftUp(n);

+    SiftUp(n);

   }

 

   method SiftUp(k: int)

@@ -76,7 +76,7 @@ class PriorityQueue {
     x := a[1];

     a[1] := a[n];

     n := n - 1;

-    call SiftDown(1);

+    SiftDown(1);

   }

 

   method SiftDown(k: int)

@@ -156,7 +156,7 @@ class PriorityQueue_Alternative {
   {

     n := n + 1;

     a[n] := x;

-    call SiftUp();

+    SiftUp();

   }

 

   method SiftUp()

@@ -189,7 +189,7 @@ class PriorityQueue_Alternative {
     x := a[1];

     a[1] := a[n];

     n := n - 1;

-    call SiftDown();

+    SiftDown();

   }

 

   method SiftDown()

diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy
index 0ee953e1..bfb588be 100644
--- a/Test/dafny1/Queue.dfy
+++ b/Test/dafny1/Queue.dfy
@@ -48,9 +48,9 @@ class Queue<T> {
     ensures Valid() && fresh(footprint - old(footprint));

     ensures contents == old(contents)[1..] + old(contents)[..1];

   {

-    call t := Front();

-    call Dequeue();

-    call Enqueue(t);

+    var t := Front();

+    Dequeue();

+    Enqueue(t);

   }

 

   method RotateAny()

@@ -62,9 +62,9 @@ class Queue<T> {
     ensures (exists i :: 0 <= i && i <= |contents| &&

               contents == old(contents)[i..] + old(contents)[..i]);

   {

-    call t := Front();

-    call Dequeue();

-    call Enqueue(t);

+    var t := Front();

+    Dequeue();

+    Enqueue(t);

   }

 

   method IsEmpty() returns (isEmpty: bool)

@@ -152,18 +152,18 @@ class Main<U> {
     var q0 := new Queue<T>.Init();

     var q1 := new Queue<T>.Init();

 

-    call q0.Enqueue(t);

-    call q0.Enqueue(u);

+    q0.Enqueue(t);

+    q0.Enqueue(u);

 

-    call q1.Enqueue(v);

+    q1.Enqueue(v);

 

     assert |q0.contents| == 2;

 

-    call w := q0.Front();

+    var w := q0.Front();

     assert w == t;

-    call q0.Dequeue();

+    q0.Dequeue();

 

-    call w := q0.Front();

+    w := q0.Front();

     assert w == u;

 

     assert |q0.contents| == 1;

@@ -179,18 +179,18 @@ class Main<U> {
     ensures fresh(q0.footprint - old(q0.footprint));

     ensures fresh(q1.footprint - old(q1.footprint));

   {

-    call q0.Enqueue(t);

-    call q0.Enqueue(u);

+    q0.Enqueue(t);

+    q0.Enqueue(u);

 

-    call q1.Enqueue(v);

+    q1.Enqueue(v);

 

     assert |q0.contents| == 2;

 

-    call w := q0.Front();

+    var w := q0.Front();

     assert w == t;

-    call q0.Dequeue();

+    q0.Dequeue();

 

-    call w := q0.Front();

+    w := q0.Front();

     assert w == u;

 

     assert |q0.contents| == 1;

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index d5b3862b..fdce6dc7 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -1,29 +1,29 @@
 // Datatypes

 

-datatype Bool { False; True; }

+datatype Bool = False | True;

 

-datatype Nat { Zero; Suc(Nat); }

+datatype Nat = Zero | Suc(Nat);

 

-datatype List { Nil; Cons(Nat, List); }

+datatype List = Nil | Cons(Nat, List);

 

-datatype Pair { Pair(Nat, Nat); }

+datatype Pair = Pair(Nat, Nat);

 

-datatype PList { PNil; PCons(Pair, PList); }

+datatype PList = PNil | PCons(Pair, PList);

 

-datatype Tree { Leaf; Node(Tree, Nat, Tree); }

+datatype Tree = Leaf | Node(Tree, Nat, Tree);

 

 // Boolean functions

 

 function not(b: Bool): Bool

 {

   match b

-  case False => #Bool.True

-  case True => #Bool.False

+  case False => True

+  case True => False

 }

 

 function and(a: Bool, b: Bool): Bool

 {

-  if a == #Bool.True && b == #Bool.True then #Bool.True else #Bool.False

+  if a == True && b == True then True else False

 }

 

 // Natural number functions

@@ -32,13 +32,13 @@ function add(x: Nat, y: Nat): Nat
 {

   match x

   case Zero => y

-  case Suc(w) => #Nat.Suc(add(w, y))

+  case Suc(w) => Suc(add(w, y))

 }

 

 function minus(x: Nat, y: Nat): Nat

 {

   match x

-  case Zero => #Nat.Zero

+  case Zero => Zero

   case Suc(a) => match y

     case Zero => x

     case Suc(b) => minus(a, b)

@@ -48,38 +48,38 @@ function eq(x: Nat, y: Nat): Bool
 {

   match x

   case Zero => (match y

-    case Zero => #Bool.True

-    case Suc(b) => #Bool.False)

+    case Zero => True

+    case Suc(b) => False)

   case Suc(a) => (match y

-    case Zero => #Bool.False

+    case Zero => False

     case Suc(b) => eq(a, b))

 }

 

 function leq(x: Nat, y: Nat): Bool

 {

   match x

-  case Zero => #Bool.True

+  case Zero => True

   case Suc(a) => match y

-    case Zero => #Bool.False

+    case Zero => False

     case Suc(b) => leq(a, b)

 }

 

 function less(x: Nat, y: Nat): Bool

 {

   match y

-  case Zero => #Bool.False

+  case Zero => False

   case Suc(b) => match x

-    case Zero => #Bool.True

+    case Zero => True

     case Suc(a) => less(a, b)

 }

 

 function min(x: Nat, y: Nat): Nat

 {

   match x

-  case Zero => #Nat.Zero

+  case Zero => Zero

   case Suc(a) => match y

-    case Zero => #Nat.Zero

-    case Suc(b) => #Nat.Suc(min(a, b))

+    case Zero => Zero

+    case Suc(b) => Suc(min(a, b))

 }

 

 function max(x: Nat, y: Nat): Nat

@@ -88,7 +88,7 @@ function max(x: Nat, y: Nat): Nat
   case Zero => y

   case Suc(a) => match y

     case Zero => x

-    case Suc(b) => #Nat.Suc(max(a, b))

+    case Suc(b) => Suc(max(a, b))

 }

 

 // List functions

@@ -97,22 +97,22 @@ function concat(xs: List, ys: List): List
 {

   match xs

   case Nil => ys

-  case Cons(x,tail) => #List.Cons(x, concat(tail, ys))

+  case Cons(x,tail) => Cons(x, concat(tail, ys))

 }

 

 function mem(x: Nat, xs: List): Bool

 {

   match xs

-  case Nil => #Bool.False

-  case Cons(y, ys) => if x == y then #Bool.True else mem(x, ys)

+  case Nil => False

+  case Cons(y, ys) => if x == y then True else mem(x, ys)

 }

 

 function delete(n: Nat, xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) =>

-    if y == n then delete(n, ys) else #List.Cons(y, delete(n, ys))

+    if y == n then delete(n, ys) else Cons(y, delete(n, ys))

 }

 

 function drop(n: Nat, xs: List): List

@@ -120,38 +120,38 @@ function drop(n: Nat, xs: List): List
   match n

   case Zero => xs

   case Suc(m) => match xs

-    case Nil => #List.Nil

+    case Nil => Nil

     case Cons(x, tail) => drop(m, tail)

 }

 

 function take(n: Nat, xs: List): List

 {

   match n

-  case Zero => #List.Nil

+  case Zero => Nil

   case Suc(m) => match xs

-    case Nil => #List.Nil

-    case Cons(x, tail) => #List.Cons(x, take(m, tail))

+    case Nil => Nil

+    case Cons(x, tail) => Cons(x, take(m, tail))

 }

 

 function len(xs: List): Nat

 {

   match xs

-  case Nil => #Nat.Zero

-  case Cons(y, ys) => #Nat.Suc(len(ys))

+  case Nil => Zero

+  case Cons(y, ys) => Suc(len(ys))

 }

 

 function count(x: Nat, xs: List): Nat

 {

   match xs

-  case Nil => #Nat.Zero

+  case Nil => Zero

   case Cons(y, ys) =>

-    if x == y then #Nat.Suc(count(x, ys)) else count(x, ys)

+    if x == y then Suc(count(x, ys)) else count(x, ys)

 }

 

 function last(xs: List): Nat

 {

   match xs

-  case Nil => #Nat.Zero

+  case Nil => Zero

   case Cons(y, ys) => match ys

     case Nil => y

     case Cons(z, zs) => last(ys)

@@ -160,39 +160,39 @@ function last(xs: List): Nat
 function mapF(xs: List): List

 {

   match xs

-  case Nil => #List.Nil

-  case Cons(y, ys) => #List.Cons(HardcodedUninterpretedFunction(y), mapF(ys))

+  case Nil => Nil

+  case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))

 }

 function HardcodedUninterpretedFunction(n: Nat): Nat;

 

 function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) =>

-    if whilePredicate(hardcodedResultOfP, y) == #Bool.True

-    then #List.Cons(y, takeWhileAlways(hardcodedResultOfP, ys))

-    else #List.Nil

+    if whilePredicate(hardcodedResultOfP, y) == True

+    then Cons(y, takeWhileAlways(hardcodedResultOfP, ys))

+    else Nil

 }

 function whilePredicate(result: Bool, arg: Nat): Bool { result }

 

 function dropWhileAlways(hardcodedResultOfP: Bool, xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) =>

-    if whilePredicate(hardcodedResultOfP, y) == #Bool.True

+    if whilePredicate(hardcodedResultOfP, y) == True

     then dropWhileAlways(hardcodedResultOfP, ys)

-    else #List.Cons(y, ys)

+    else Cons(y, ys)

 }

 

 function filterP(xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) =>

-    if HardcodedUninterpretedPredicate(y) == #Bool.True

-    then #List.Cons(y, filterP(ys))

+    if HardcodedUninterpretedPredicate(y) == True

+    then Cons(y, filterP(ys))

     else filterP(ys)

 }

 function HardcodedUninterpretedPredicate(n: Nat): Bool;

@@ -200,37 +200,37 @@ function HardcodedUninterpretedPredicate(n: Nat): Bool;
 function insort(n: Nat, xs: List): List

 {

   match xs

-  case Nil => #List.Cons(n, #List.Nil)

+  case Nil => Cons(n, Nil)

   case Cons(y, ys) =>

-    if leq(n, y) == #Bool.True

-    then #List.Cons(n, #List.Cons(y, ys))

-    else #List.Cons(y, ins(n, ys))

+    if leq(n, y) == True

+    then Cons(n, Cons(y, ys))

+    else Cons(y, ins(n, ys))

 }

 

 function ins(n: Nat, xs: List): List

 {

   match xs

-  case Nil => #List.Cons(n, #List.Nil)

+  case Nil => Cons(n, Nil)

   case Cons(y, ys) =>

-    if less(n, y) == #Bool.True

-    then #List.Cons(n, #List.Cons(y, ys))

-    else #List.Cons(y, ins(n, ys))

+    if less(n, y) == True

+    then Cons(n, Cons(y, ys))

+    else Cons(y, ins(n, ys))

 }

 

 function ins1(n: Nat, xs: List): List

 {

   match xs

-  case Nil => #List.Cons(n, #List.Nil)

+  case Nil => Cons(n, Nil)

   case Cons(y, ys) =>

     if n == y

-    then #List.Cons(y, ys)

-    else #List.Cons(y, ins1(n, ys))

+    then Cons(y, ys)

+    else Cons(y, ins1(n, ys))

 }

 

 function sort(xs: List): List

 {

   match xs

-  case Nil => #List.Nil

+  case Nil => Nil

   case Cons(y, ys) => insort(y, sort(ys))

 }

 

@@ -239,17 +239,17 @@ function sort(xs: List): List
 function zip(a: List, b: List): PList

 {

   match a

-  case Nil => #PList.PNil

+  case Nil => PNil

   case Cons(x, xs) => match b

-    case Nil => #PList.PNil

-    case Cons(y, ys) => #PList.PCons(#Pair.Pair(x, y), zip(xs, ys))

+    case Nil => PNil

+    case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))

 }

 

 function zipConcat(x: Nat, xs: List, more: List): PList

 {

   match more

-  case Nil => #PList.PNil

-  case Cons(y, ys) => #PList.PCons(#Pair.Pair(x, y), zip(xs, ys))

+  case Nil => PNil

+  case Cons(y, ys) => PCons(Pair.Pair(x, y), zip(xs, ys))

 }

 

 // Binary tree functions

@@ -257,15 +257,15 @@ function zipConcat(x: Nat, xs: List, more: List): PList
 function height(t: Tree): Nat

 {

   match t

-  case Leaf => #Nat.Zero

-  case Node(l, x, r) => #Nat.Suc(max(height(l), height(r)))

+  case Leaf => Zero

+  case Node(l, x, r) => Suc(max(height(l), height(r)))

 }

 

 function mirror(t: Tree): Tree

 {

   match t

-  case Leaf => #Tree.Leaf

-  case Node(l, x, r) => #Tree.Node(mirror(r), x, mirror(l))

+  case Leaf => Leaf

+  case Node(l, x, r) => Node(mirror(r), x, mirror(l))

 }

 

 // The theorems to be proved

@@ -281,24 +281,24 @@ ghost method P2()
 }

 

 ghost method P3()

-  ensures (forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == #Bool.True);

+  ensures (forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True);

 {

 }

 

 ghost method P4()

-  ensures (forall n, xs :: add(#Nat.Suc(#Nat.Zero), count(n, xs)) == count(n, #List.Cons(n, xs)));

+  ensures (forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs)));

 {

 }

 

 ghost method P5()

   ensures (forall n, xs, x ::

-    add(#Nat.Suc(#Nat.Zero), count(n, xs)) == count(n, #List.Cons(x, xs))

+    add(Suc(Zero), count(n, xs)) == count(n, Cons(x, xs))

     ==> n == x);

 {

 }

 

 ghost method P6()

-  ensures (forall m, n :: minus(n, add(n, m)) == #Nat.Zero);

+  ensures (forall m, n :: minus(n, add(n, m)) == Zero);

 {

 }

 

@@ -318,12 +318,12 @@ ghost method P9()
 }

 

 ghost method P10()

-  ensures (forall m :: minus(m, m) == #Nat.Zero);

+  ensures (forall m :: minus(m, m) == Zero);

 {

 }

 

 ghost method P11()

-  ensures (forall xs :: drop(#Nat.Zero, xs) == xs);

+  ensures (forall xs :: drop(Zero, xs) == xs);

 {

 }

 

@@ -333,7 +333,7 @@ ghost method P12()
 }

 

 ghost method P13()

-  ensures (forall n, x, xs :: drop(#Nat.Suc(n), #List.Cons(x, xs)) == drop(n, xs));

+  ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs));

 {

 }

 

@@ -343,22 +343,22 @@ ghost method P14()
 }

 

 ghost method P15()

-  ensures (forall x, xs :: len(ins(x, xs)) == #Nat.Suc(len(xs)));

+  ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs)));

 {

 }

 

 ghost method P16()

-  ensures (forall x, xs :: xs == #List.Nil ==> last(#List.Cons(x, xs)) == x);

+  ensures (forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x);

 {

 }

 

 ghost method P17()

-  ensures (forall n :: leq(n, #Nat.Zero) == #Bool.True <==> n == #Nat.Zero);

+  ensures (forall n :: leq(n, Zero) == True <==> n == Zero);

 {

 }

 

 ghost method P18()

-  ensures (forall i, m :: less(i, #Nat.Suc(add(i, m))) == #Bool.True);

+  ensures (forall i, m :: less(i, Suc(add(i, m))) == True);

 {

 }

 

@@ -371,15 +371,15 @@ ghost method P20()
   ensures (forall xs :: len(sort(xs)) == len(xs));

 {

   // proving this theorem requires an additional lemma:

-  assert (forall k, ks :: len(ins(k, ks)) == len(#List.Cons(k, ks)));

+  assert (forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks)));

   // ...and one manually introduced case study:

   assert (forall ys ::

-           sort(ys) == #List.Nil ||

-           (exists z, zs :: sort(ys) == #List.Cons(z, zs)));

+           sort(ys) == Nil ||

+           (exists z, zs :: sort(ys) == Cons(z, zs)));

 }

 

 ghost method P21()

-  ensures (forall n, m :: leq(n, add(n, m)) == #Bool.True);

+  ensures (forall n, m :: leq(n, add(n, m)) == True);

 {

 }

 

@@ -394,37 +394,37 @@ ghost method P23()
 }

 

 ghost method P24()

-  ensures (forall a, b :: max(a, b) == a <==> leq(b, a) == #Bool.True);

+  ensures (forall a, b :: max(a, b) == a <==> leq(b, a) == True);

 {

 }

 

 ghost method P25()

-  ensures (forall a, b :: max(a, b) == b <==> leq(a, b) == #Bool.True);

+  ensures (forall a, b :: max(a, b) == b <==> leq(a, b) == True);

 {

 }

 

 ghost method P26()

-  ensures (forall x, xs, ys :: mem(x, xs) == #Bool.True ==> mem(x, concat(xs, ys)) == #Bool.True);

+  ensures (forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True);

 {

 }

 

 ghost method P27()

-  ensures (forall x, xs, ys :: mem(x, ys) == #Bool.True ==> mem(x, concat(xs, ys)) == #Bool.True);

+  ensures (forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True);

 {

 }

 

 ghost method P28()

-  ensures (forall x, xs :: mem(x, concat(xs, #List.Cons(x, #List.Nil))) == #Bool.True);

+  ensures (forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True);

 {

 }

 

 ghost method P29()

-  ensures (forall x, xs :: mem(x, ins1(x, xs)) == #Bool.True);

+  ensures (forall x, xs :: mem(x, ins1(x, xs)) == True);

 {

 }

 

 ghost method P30()

-  ensures (forall x, xs :: mem(x, ins(x, xs)) == #Bool.True);

+  ensures (forall x, xs :: mem(x, ins(x, xs)) == True);

 {

 }

 

@@ -439,43 +439,43 @@ ghost method P32()
 }

 

 ghost method P33()

-  ensures (forall a, b :: min(a, b) == a <==> leq(a, b) == #Bool.True);

+  ensures (forall a, b :: min(a, b) == a <==> leq(a, b) == True);

 {

 }

 

 ghost method P34()

-  ensures (forall a, b :: min(a, b) == b <==> leq(b, a) == #Bool.True);

+  ensures (forall a, b :: min(a, b) == b <==> leq(b, a) == True);

 {

 }

 

 ghost method P35()

-  ensures (forall xs :: dropWhileAlways(#Bool.False, xs) == xs);

+  ensures (forall xs :: dropWhileAlways(False, xs) == xs);

 {

 }

 

 ghost method P36()

-  ensures (forall xs :: takeWhileAlways(#Bool.True, xs) == xs);

+  ensures (forall xs :: takeWhileAlways(True, xs) == xs);

 {

 }

 

 ghost method P37()

-  ensures (forall x, xs :: not(mem(x, delete(x, xs))) == #Bool.True);

+  ensures (forall x, xs :: not(mem(x, delete(x, xs))) == True);

 {

 }

 

 ghost method P38()

-  ensures (forall n, xs :: count(n, concat(xs, #List.Cons(n, #List.Nil))) == #Nat.Suc(count(n, xs)));

+  ensures (forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs)));

 {

 }

 

 ghost method P39()

   ensures (forall n, x, xs ::

-            add(count(n, #List.Cons(x, #List.Nil)), count(n, xs)) == count(n, #List.Cons(x, xs)));

+            add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs)));

 {

 }

 

 ghost method P40()

-  ensures (forall xs :: take(#Nat.Zero, xs) == #List.Nil);

+  ensures (forall xs :: take(Zero, xs) == Nil);

 {

 }

 

@@ -485,7 +485,7 @@ ghost method P41()
 }

 

 ghost method P42()

-  ensures (forall n, x, xs :: take(#Nat.Suc(n), #List.Cons(x, xs)) == #List.Cons(x, take(n, xs)));

+  ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs)));

 {

 }

 

@@ -496,19 +496,19 @@ ghost method P43(p: Bool)
 }

 

 ghost method P44()

-  ensures (forall x, xs, ys :: zip(#List.Cons(x, xs), ys) == zipConcat(x, xs, ys));

+  ensures (forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys));

 {

 }

 

 ghost method P45()

   ensures (forall x, xs, y, ys ::

-            zip(#List.Cons(x, xs), #List.Cons(y, ys)) ==

-            #PList.PCons(#Pair.Pair(x, y), zip(xs, ys)));

+            zip(Cons(x, xs), Cons(y, ys)) ==

+            PCons(Pair.Pair(x, y), zip(xs, ys)));

 {

 }

 

 ghost method P46()

-  ensures (forall ys :: zip(#List.Nil, ys) == #PList.PNil);

+  ensures (forall ys :: zip(Nil, ys) == PNil);

 {

 }

 

@@ -530,27 +530,27 @@ ghost method P54()
 }

 

 ghost method P65()

-  ensures (forall i, m :: less(i, #Nat.Suc(add(m, i))) == #Bool.True);

+  ensures (forall i, m :: less(i, Suc(add(m, i))) == True);

 {

   if (*) {

     // the proof of this theorem follows from two lemmas:

-    assert (forall i, m :: less(i, #Nat.Suc(add(i, m))) == #Bool.True);

+    assert (forall i, m :: less(i, Suc(add(i, m))) == True);

     assert (forall m, n :: add(m, n) == add(n, m));

   } else {

     // a different way to prove it uses the following lemma:

-    assert (forall x,y :: add(x, #Nat.Suc(y)) == #Nat.Suc(add(x,y)));

+    assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));

   }

 }

 

 ghost method P67()

-  ensures (forall m, n :: leq(n, add(m, n)) == #Bool.True);

+  ensures (forall m, n :: leq(n, add(m, n)) == True);

 {

   if (*) {

     // the proof of this theorem follows from two lemmas:

-    assert (forall m, n :: leq(n, add(n, m)) == #Bool.True);

+    assert (forall m, n :: leq(n, add(n, m)) == True);

     assert (forall m, n :: add(m, n) == add(n, m));

   } else {

     // a different way to prove it uses the following lemma:

-    assert (forall x,y :: add(x, #Nat.Suc(y)) == #Nat.Suc(add(x,y)));

+    assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));

   }

 }

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 0d69b1b8..8da32b05 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -10,6 +10,8 @@ class Node {
   ghost var pathFromRoot: Path;

 }

 

+datatype Path = Empty | Extend(Path, Node);

+

 class Main {

   method RecursiveMark(root: Node, ghost S: set<Node>)

     requires root in S;

@@ -26,7 +28,7 @@ class Main {
                 n.childrenVisited == old(n.childrenVisited) &&

                 n.children == old(n.children));

   {

-    call RecursiveMarkWorker(root, S, {});

+    RecursiveMarkWorker(root, S, {});

   }

 

   method RecursiveMarkWorker(root: Node, ghost S: set<Node>, ghost stackNodes: set<Node>)

@@ -67,7 +69,7 @@ class Main {
       {

         var c := root.children[i];

         if (c != null) {

-          call RecursiveMarkWorker(c, S, stackNodes + {root});

+          RecursiveMarkWorker(c, S, stackNodes + {root});

         }

         i := i + 1;

       }

@@ -182,7 +184,7 @@ class Main {
   {

     var t := root;

     var p: Node := null;  // parent of t in original graph

-    ghost var path := #Path.Empty;

+    ghost var path := Path.Empty;

     t.marked := true;

     t.pathFromRoot := path;

     ghost var stackNodes := [];

@@ -256,7 +258,7 @@ class Main {
         t.children := t.children[..t.childrenVisited] + [p] + t.children[t.childrenVisited + 1..];

         p := t;

         stackNodes := stackNodes + [t];

-        path := #Path.Extend(path, t);

+        path := Path.Extend(path, t);

         t := newT;

         t.marked := true;

         t.pathFromRoot := path;

@@ -265,8 +267,3 @@ class Main {
     }

   }

 }

-

-datatype Path {

-  Empty;

-  Extend(Path, Node);

-}

diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy
index 7828a54e..56a64bd6 100644
--- a/Test/dafny1/SeparationLogicList.dfy
+++ b/Test/dafny1/SeparationLogicList.dfy
@@ -28,7 +28,7 @@ class Node<T> {
       l.next := null;

       S := {l};

     } else {

-      call l, S := Cons(x, null, [], {});

+      l, S := Cons(x, null, [], {});

     }

   }

 

@@ -75,7 +75,7 @@ class ListNode<T> {
       l.Repr := {l};

       l.Contents := [x];

     } else {

-      call l := Cons(x, null);

+      l := Cons(x, null);

     }

   }

 

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 8d51bdd1..ad39e3f2 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,27 +1,23 @@
-datatype List {

-  Nil;

-  Cons(Expr, List);

-}

+datatype List = Nil | Cons(Expr, List);

 

-datatype Expr {

-  Const(int);

-  Var(int);

+datatype Expr =

+  Const(int) |

+  Var(int) |

   Nary(int, List);

-}

 

 static function Subst(e: Expr, v: int, val: int): Expr

 {

   match e

   case Const(c) => e

-  case Var(x) => if x == v then #Expr.Const(val) else e

-  case Nary(op, args) => #Expr.Nary(op, SubstList(args, v, val))

+  case Var(x) => if x == v then Expr.Const(val) else e

+  case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))

 }

 

 static function SubstList(l: List, v: int, val: int): List

 {

   match l

   case Nil => l

-  case Cons(e, tail) => #List.Cons(Subst(e, v, val), SubstList(tail, v, val))

+  case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))

 }

 

 static ghost method Theorem(e: Expr, v: int, val: int)

@@ -31,7 +27,7 @@ static ghost method Theorem(e: Expr, v: int, val: int)
     case Const(c) =>

     case Var(x) =>

     case Nary(op, args) =>

-      call Lemma(args, v, val);

+      Lemma(args, v, val);

   }

 }

 

@@ -41,26 +37,25 @@ static ghost method Lemma(l: List, v: int, val: int)
   match l {

     case Nil =>

     case Cons(e, tail) =>

-      call Theorem(e, v, val);

-      call Lemma(tail, v, val);

+      Theorem(e, v, val);

+      Lemma(tail, v, val);

   }

 }

 

 // -------------------------------

 

-datatype Expression {

-  Const(int);

-  Var(int);

+datatype Expression =

+  Const(int) |

+  Var(int) |

   Nary(int, seq<Expression>);

-}

 

 static function Substitute(e: Expression, v: int, val: int): Expression

   decreases e;

 {

   match e

   case Const(c) => e

-  case Var(x) => if x == v then #Expression.Const(val) else e

-  case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val))

+  case Var(x) => if x == v then Expression.Const(val) else e

+  case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))

 }

 

 static function SubstSeq(/*ghost*/ parent: Expression,

@@ -80,11 +75,11 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
     case Var(x) =>

     case Nary(op, args) =>

       ghost var seArgs := SubstSeq(e, args, v, val);

-      call LemmaSeq(e, args, v, val);

+      LemmaSeq(e, args, v, val);

 

       ghost var se := Substitute(e, v, val);

       ghost var seArgs2 := SubstSeq(se, seArgs, v, val);

-      call LemmaSeq(se, seArgs, v, val);

+      LemmaSeq(se, seArgs, v, val);

 

       var N := |args|;

       var j := 0;

@@ -92,14 +87,14 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
         invariant j <= N;

         invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);

       {

-        call TheoremSeq(args[j], v, val);

+        TheoremSeq(args[j], v, val);

         j := j + 1;

       }

       assert seArgs == seArgs2;

   }

 }

 

-static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, v: int, val: int)

+static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)

   requires (forall a :: a in q ==> a < parent);

   ensures |SubstSeq(parent, q, v, val)| == |q|;

   ensures (forall k :: 0 <= k && k < |q| ==>

@@ -107,6 +102,6 @@ static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,
 {

   if (q == []) {

   } else {

-    call LemmaSeq(parent, q[..|q|-1], v, val);

+    LemmaSeq(parent, q[..|q|-1], v, val);

   }

 }

diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy
index 2fecaee5..7ed7ce9b 100644
--- a/Test/dafny1/SumOfCubes.dfy
+++ b/Test/dafny1/SumOfCubes.dfy
@@ -10,19 +10,19 @@ class SumOfCubes {
     requires 0 <= n && n <= m;

     ensures r == SumEmUp(n, m);

   {

-    call a := SocuFromZero(m);

-    call b := SocuFromZero(n);

+    var a := SocuFromZero(m);

+    var b := SocuFromZero(n);

     r := a - b;

-    call Lemma0(n, m);

+    Lemma0(n, m);

   }

 

   static method SocuFromZero(k: int) returns (r: int)

     requires 0 <= k;

     ensures r == SumEmUp(0, k);

   {

-    call g := Gauss(k);

+    var g := Gauss(k);

     r := g * g;

-    call Lemma1(k);

+    Lemma1(k);

   }

 

   ghost static method Lemma0(n: int, m: int)

@@ -36,9 +36,9 @@ class SumOfCubes {
     {

       k := k + 1;

     }

-    call Lemma3(0, n);

-    call Lemma3(n, k);

-    call Lemma3(0, k);

+    Lemma3(0, n);

+    Lemma3(n, k);

+    Lemma3(0, k);

   }

 

   static function GSum(k: int): int

@@ -52,7 +52,7 @@ class SumOfCubes {
     ensures r == GSum(k);

   {

     r := k * (k - 1) / 2;

-    call Lemma2(k);

+    Lemma2(k);

   }

 

   ghost static method Lemma1(k: int)

@@ -64,10 +64,10 @@ class SumOfCubes {
       invariant i <= k;

       invariant SumEmDown(0, i) == GSum(i) * GSum(i);

     {

-      call Lemma2(i);

+      Lemma2(i);

       i := i + 1;

     }

-    call Lemma3(0, k);

+    Lemma3(0, k);

   }

 

   ghost static method Lemma2(k: int)

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 49f5a075..0aa36a10 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -58,10 +58,10 @@ class Ackermann {
     if (m == 0) {

       r := n + 1;

     } else if (n == 0) {

-      call r := ComputeAck(m - 1, 1);

+      r := ComputeAck(m - 1, 1);

     } else {

-      call s := ComputeAck(m, n - 1);

-      call r := ComputeAck(m - 1, s);

+      var s := ComputeAck(m, n - 1);

+      r := ComputeAck(m - 1, s);

     }

   }

 }

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index f576850e..a94283e6 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -1,68 +1,56 @@
 // ------------------ generic list, non-generic tree

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

-datatype Tree {

-  Node(int, List<Tree>);

-}

+datatype Tree = Node(int, List<Tree>);

 

 static function Inc(t: Tree): Tree

 {

   match t

-  case Node(n, children) => #Tree.Node(n+1, ForestInc(children))

+  case Node(n, children) => Tree.Node(n+1, ForestInc(children))

 }

 

 static function ForestInc(forest: List<Tree>): List<Tree>

 {

   match forest

   case Nil => forest

-  case Cons(tree, tail) => #List.Cons(Inc(tree), ForestInc(tail))

+  case Cons(tree, tail) => List.Cons(Inc(tree), ForestInc(tail))

 }

 

 // ------------------ generic list, generic tree (but GInc defined only for GTree<int>

 

-datatype GTree<T> {

-  Node(T, List<GTree<T>>);

-}

+datatype GTree<T> = Node(T, List<GTree<T>>);

 

 static function GInc(t: GTree<int>): GTree<int>

 {

   match t

-  case Node(n, children) => #GTree.Node(n+1, GForestInc(children))

+  case Node(n, children) => GTree.Node(n+1, GForestInc(children))

 }

 

 static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>

 {

   match forest

   case Nil => forest

-  case Cons(tree, tail) => #List.Cons(GInc(tree), GForestInc(tail))

+  case Cons(tree, tail) => List.Cons(GInc(tree), GForestInc(tail))

 }

 

 // ------------------ non-generic structures

 

-datatype TreeList {

-  Nil;

-  Cons(OneTree, TreeList);

-}

+datatype TreeList = Nil | Cons(OneTree, TreeList);

 

-datatype OneTree {

-  Node(int, TreeList);

-}

+datatype OneTree = Node(int, TreeList);

 

 static function XInc(t: OneTree): OneTree

 {

   match t

-  case Node(n, children) => #OneTree.Node(n+1, XForestInc(children))

+  case Node(n, children) => OneTree.Node(n+1, XForestInc(children))

 }

 

 static function XForestInc(forest: TreeList): TreeList

 {

   match forest

   case Nil => forest

-  case Cons(tree, tail) => #TreeList.Cons(XInc(tree), XForestInc(tail))

+  case Cons(tree, tail) => TreeList.Cons(XInc(tree), XForestInc(tail))

 }

 

 // ------------------ fun with recursive functions

@@ -77,7 +65,7 @@ function len<T>(l: List<T>): int
 function SingletonList<T>(h: T): List<T>

   ensures len(SingletonList(h)) == 1;

 {

-  #List.Cons(h, #List.Nil)

+  List.Cons(h, List.Nil)

 }

 

 function Append<T>(a: List<T>, b: List<T>): List<T>

@@ -85,7 +73,7 @@ function Append<T>(a: List<T>, b: List<T>): List<T>
 {

   match a

   case Nil => b

-  case Cons(h,t) => #List.Cons(h, Append(t, b))

+  case Cons(h,t) => List.Cons(h, Append(t, b))

 }

 

 function Rotate<T>(n: int, l: List<T>): List<T>

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>)

diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
index 52cddaac..c7e4bc63 100644
--- a/Test/dafny1/pow2.dfy
+++ b/Test/dafny1/pow2.dfy
@@ -36,7 +36,7 @@ ghost method Lemma(n: int)
   ensures pow2_slow(n) == Square(pow2_slow(n/2));

 {

   if (n != 0) {

-    call Lemma(n-2);

+    Lemma(n-2);

   }

 }

 

@@ -46,9 +46,9 @@ ghost method Theorem(n: int)
 {

   if (n == 0) {

   } else if (IsEven(n)) {

-    call Lemma(n);

-    call Theorem(n/2);

+    Lemma(n);

+    Theorem(n/2);

   } else {

-    call Theorem(n-1);

+    Theorem(n-1);

   }

 }