1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 39e14ea5..0a4d541d 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -515,8 +515,8 @@ ghost method P46()
 ghost method P47()
   ensures (forall a :: height(mirror(a)) == height(a));
 {
-  // proving this theorem requires an additional lemma:
-  assert (forall x,y :: max(x,y) == max(y,x));
+  // proving this theorem requires a previously proved lemma:
+  P23();
 }
 
 // ...