diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index ce0535337575a86a696c5a902ca2960a7e8bc658..3ec5fcf2a79758e74d46047ab081f53e94dd773d 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -106,7 +106,7 @@ object Extractors {
       }))
       case fi @ FunctionInvocation(fd, args) => Some((args, (as => FunctionInvocation(fd, as).setPos(fi))))
       case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, (as => MethodInvocation(as.head, cd, tfd, as.tail).setPos(mi))))
-      case fa @ Application(caller, args) => Some((caller +: args), (as => Application(as.head, as.tail).setPos(fa)))
+      case fa @ Application(caller, args) => Some((caller +: args), (as => application(as.head, as.tail).setPos(fa)))
       case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
       case And(args) => Some((args, and))
       case Or(args) => Some((args, or))
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 665cf21f0e6bd47b7c64e0b9218c2ebfcd70e3e0..6ecd9f720dc1993fad20b1e346debfc1b6ecaecb 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -69,7 +69,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
               (a, kind, cond)
             case a @ Assert(cond, None, _) => (a, VCAssert, cond)
             // Only triggered for inner ensurings, general postconditions are handled by generatePostconditions
-            case a @ Ensuring(body, post) => (a, VCAssert, Application(post, Seq(body)))
+            case a @ Ensuring(body, post) => (a, VCAssert, application(post, Seq(body)))
           }(body)
 
           calls.map {