Made /rewriteFocalPredicates:1 the default

1 files changed, 3 insertions, 3 deletions

diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 6f541396..4f8b35ec 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -157,11 +157,11 @@ colemma Filter_IsSubStream(s: Stream, P: Predicate)
     calc {

       true;

     ==  { Filter_IsSubStream(s.tail, P); }  // induction hypothesis

-      IsSubStream#[_k-1](Filter(s.tail, P), s.tail);

+      IsSubStream(Filter(s.tail, P), s.tail);

     == // { assert Filter(s.tail, h) == Filter(s, h).tail; }

-      IsSubStream#[_k-1](Filter(s, P).tail, s.tail);

+      IsSubStream(Filter(s, P).tail, s.tail);

     ==> { Lemma_TailSubStreamK(Filter(s, P).tail, s, _k-1); }

-      IsSubStream#[_k-1](Filter(s, P).tail, s);

+      IsSubStream(Filter(s, P).tail, s);

     }

     calc {

       In(Filter(s, P).head, s);