From cfe05df94a5ccb6025c94bd21b09bfc1240de756 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 2 Oct 2015 18:56:13 -0700
Subject: Made /rewriteFocalPredicates:1 the default

---
 Test/dafny3/Filter.dfy | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Test/dafny3')

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);
-- 
cgit v1.2.3