5 files changed, 12 insertions, 12 deletions
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 8df1a7c5..2063eec4 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -44,17 +44,17 @@ class SoWellformed {
     c := true;
   }
 
-  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);
+  method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
     requires next != null;
     modifies this;
     ensures next.xyz < 100;  // error: may not be well-defined (if body sets next to null)
 
-  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+  method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
     requires next != null;
     modifies s;
     ensures next.xyz < 100;  // error: may not be well-defined (if this in s and body sets next to null)
 
-  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+  method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
     requires next != null && this !in s;
     modifies s;
     ensures next.xyz < 100;  // fine
@@ -175,7 +175,7 @@ class StatementTwoShoes {
   }
 
   function G(w: int): int { 5 }
-  function method H(x: int): int;
+  function method H(x: int): int
 
   method V(s: set<StatementTwoShoes>, a: int, b: int)
     modifies s;
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 53d3bf03..e56b4122 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -42,7 +42,7 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
   r := t1;
 }
 
-function method FenEric<T>(t0: T, t1: T): T;
+function method FenEric<T>(t0: T, t1: T): T
 
 datatype Pair<T> = Pr(T, T);
 
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index d4d1dfcf..f31935af 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -87,7 +87,7 @@ class Termination {
     }
   }
 
-  method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);
+  method Traverse<T>(a: List<T>) returns (val: T, b: List<T>)
     requires a != List.Nil;
     ensures a == List.Cons(val, b);
 }
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 2bedd37d..710e9838 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -88,7 +88,7 @@ method N() returns (k: MyClass)
   k := new MyClass;
 }
 
-function NF(): MyClass;
+function NF(): MyClass
 
 function TakesADatatype(a: List): int { 12 }
 
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a3698dc0..8f3f8b87 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -17,7 +17,7 @@ class C<U> {
     assert kz && (G() || !G());
   }
 
-  function G<Y>(): Y;
+  function G<Y>(): Y
 }
 
 class SetTest {
@@ -99,7 +99,7 @@ class CClient {
 
 // -------------------------
 
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool;
+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
   requires c == c || c in people;
 
 method FindCelebrity3(people: set<int>, ghost c: int)
@@ -110,7 +110,7 @@ method FindCelebrity3(people: set<int>, ghost c: int)
   b := F(c, people);
 }
 
-static function F(c: int, people: set<int>): bool;
+static function F(c: int, people: set<int>): bool
   requires IsCelebrity(c, people);
 
 function RogerThat<G>(g: G): G
@@ -153,8 +153,8 @@ method LoopyRoger(n: int)
 
 class TyKn_C<T> {
   var x: T;
-  function G(): T;
-  method M() returns (t: T);
+  function G(): T
+  method M() returns (t: T)
 }
 
 class TyKn_K {