1 files changed, 7 insertions, 12 deletions
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 11c8c878..ad39e3f2 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,13 +1,9 @@
-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
 {
@@ -48,11 +44,10 @@ static ghost method Lemma(l: List, v: int, val: int)
 
 // -------------------------------
 
-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;