3 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 74512e01..21b895aa 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,6 +1,6 @@
 // Celebrity example, inspired by the Rodin tutorial
 
-static function method Knows<Person>(a: Person, b: Person): bool;
+static function method Knows<Person>(a: Person, b: Person): bool
   requires a != b;  // forbid asking about the reflexive case
 
 static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index fdce6dc7..39e14ea5 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -163,7 +163,7 @@ function mapF(xs: List): List
   case Nil => Nil
   case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))
 }
-function HardcodedUninterpretedFunction(n: Nat): Nat;
+function HardcodedUninterpretedFunction(n: Nat): Nat
 
 function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List
 {
@@ -195,7 +195,7 @@ function filterP(xs: List): List
     then Cons(y, filterP(ys))
     else filterP(ys)
 }
-function HardcodedUninterpretedPredicate(n: Nat): Bool;
+function HardcodedUninterpretedPredicate(n: Nat): Bool
 
 function insort(n: Nat, xs: List): List
 {
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 189ff2b5..c8419890 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -29,7 +29,7 @@ class UltraFilter<G> {
   }
 
   // Dafny currently does not have a set comprehension expression, so this method stub will have to do
-  method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>);
+  method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)
     ensures (forall X :: X in h <==> M + X in f);
 
   method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)