Dafny: Cleaned up proof of RevConcat in test case

1 files changed, 0 insertions, 2 deletions

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index c9a9f3b7..211afd83 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -602,7 +602,6 @@ ghost method Lemma_RevConcat(xs: List, ys: List)
     case Nil =>

       assert forall ws :: concat(ws, Nil) == ws;

     case Cons(t, rest) =>

-      Lemma_RevConcat(rest, ys);

       assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);

   }

 }

@@ -614,6 +613,5 @@ ghost method Theorem(xs: List)
     case Nil =>

     case Cons(t, rest) =>

       Lemma_RevConcat(reverse(rest), Cons(t, Nil));

-      Theorem(rest);

   }

 }