diff --git a/src/main/scala/leon/verification/GroupedTactic.scala b/src/main/scala/leon/verification/GroupedTactic.scala
index 6ef63a8f8cdc4e9a21171e06e501387f8e684e52..8bd957037539701ff3b4d06a6654477e6b4492a6 100644
--- a/src/main/scala/leon/verification/GroupedTactic.scala
+++ b/src/main/scala/leon/verification/GroupedTactic.scala
@@ -20,7 +20,9 @@ class GroupedTactic(vctx: VerificationContext) extends Tactic(vctx) {
         } yield {
           implies(
             precOrTrue(inComp),
-            application(p, Seq(b))
+            // @mk: Don't know which one is better. Inline the body, or have it as a fun. app?
+            //application(p, Seq(b))
+            application(p, Seq(FunctionInvocation(inComp.typedWithDef, inComp.params map { _.toVariable })))
           )
         }