1 files changed, 10 insertions, 21 deletions
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 21f0dda8..9df11a67 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -13,37 +13,26 @@ class C {
   }
 }
 
-datatype D {
-  A;
-}
-
-datatype Nothing {  // error: no grounding constructor
-}
+datatype D = A;
 
-datatype NeverendingList {  // error: no grounding constructor
-  Cons(int, NeverendingList);
-}
+datatype NeverendingList = Cons(int, NeverendingList);  // error: no grounding constructor
 
-datatype MutuallyRecursiveDataType<T> {
-  FromANumber(int);  // this is the base case
+datatype MutuallyRecursiveDataType<T> =
+  FromANumber(int) |  // this is the base case
   Else(TheCounterpart<T>, C);
-}
 
-datatype TheCounterpart<T> {
-  TreeLike(TheCounterpart<T>, TheCounterpart<T>);
+datatype TheCounterpart<T> =
+  TreeLike(TheCounterpart<T>, TheCounterpart<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
+datatype ReverseOrder_MutuallyRecursiveDataType<T> =
+  FromANumber(int) |  // this is the base case
   Else(ReverseOrder_TheCounterpart<T>, C);
-}
 
-datatype ReverseOrder_TheCounterpart<T> {
-  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>);
+datatype ReverseOrder_TheCounterpart<T> =
+  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>) |
   More(ReverseOrder_MutuallyRecursiveDataType<T>);
-}
 
 // ---------------------