1 files changed, 6 insertions, 6 deletions
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 01c2a0a5..b44f4d68 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -16,26 +16,26 @@ class C {
   }
 }
 
-datatype D = A;
+datatype D = A
 
-datatype NeverendingList = Cons(int, NeverendingList);  // error: no grounding constructor
+datatype NeverendingList = Cons(int, NeverendingList)  // error: no grounding constructor
 
 datatype MutuallyRecursiveDataType<T> =
   FromANumber(int) |  // this is the base case
-  Else(TheCounterpart<T>, C);
+  Else(TheCounterpart<T>, C)
 
 datatype TheCounterpart<T> =
   TreeLike(TheCounterpart<T>, TheCounterpart<T>) |
-  More(MutuallyRecursiveDataType<T>);
+  More(MutuallyRecursiveDataType<T>)
 
 // these 'ReverseOrder_' order tests may be called white-box unit tests
 datatype ReverseOrder_MutuallyRecursiveDataType<T> =
   FromANumber(int) |  // this is the base case
-  Else(ReverseOrder_TheCounterpart<T>, C);
+  Else(ReverseOrder_TheCounterpart<T>, C)
 
 datatype ReverseOrder_TheCounterpart<T> =
   TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>) |
-  More(ReverseOrder_MutuallyRecursiveDataType<T>);
+  More(ReverseOrder_MutuallyRecursiveDataType<T>)
 
 // ---------------------