Compile lambda functions and apply expressions, and change let expr compilation

1 files changed, 3 insertions, 3 deletions

diff --git a/Test/hofs/Renaming.dfy b/Test/hofs/Renaming.dfy
index 7a3f69a5..8a2dc03a 100644
--- a/Test/hofs/Renaming.dfy
+++ b/Test/hofs/Renaming.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function OnId(f : (bool -> bool) -> int) : int
@@ -16,9 +16,9 @@ method Equal() {
 }
 
 method K<A,B>(P : (A -> A) -> bool)
+  requires P.requires(x => x);
+  requires P(y => y);
 {
-  assume P.requires(x => x);
-  assume P(y => y);
   assert P(z => z);
   assert (x => y => x) == ((a : A) => (b : B) => a);
 }