diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 57a7d445105e41defb7adcd47da758ea1d976eaf..a3d00ad98624de40611d810ed1f37f011c12f892 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -3,7 +3,6 @@
 package leon
 package purescala
 
-import sun.reflect.generics.tree.ReturnType
 import utils.Library
 import Common._
 import Expressions._
@@ -46,7 +45,7 @@ object Definitions {
    *  The optional tpe, if present, overrides the type of the underlying Identifier id
    *  This is useful to instantiate argument types of polymorphic functions
    */
-  case class ValDef(val id: Identifier, val isLazy: Boolean = false) extends Definition with Typed {
+  case class ValDef(id: Identifier, isLazy: Boolean = false) extends Definition with Typed {
     self: Serializable =>
 
     val getType = id.getType
@@ -154,7 +153,7 @@ object Definitions {
   
   object UnitDef {
     def apply(id: Identifier, modules : Seq[ModuleDef]) : UnitDef = 
-      UnitDef(id,Nil, Nil, modules,true)
+      UnitDef(id, Nil, Nil, modules, true)
   }
   
   /** Objects work as containers for class definitions, functions (def's) and
@@ -479,11 +478,20 @@ object Definitions {
 
     def translated(e: Expr): Expr = instantiateType(e, typesMap, paramsMap)
 
+    /** A mapping from this [[TypedFunDef]]'s formal parameters to real arguments
+      *
+      * @param realArgs The arguments to which the formal argumentas are mapped
+      * */
     def paramSubst(realArgs: Seq[Expr]) = {
       require(realArgs.size == params.size)
       (paramIds zip realArgs).toMap
     }
 
+    /** Substitute this [[TypedFunDef]]'s formal parameters with real arguments in some expression
+     *
+     * @param realArgs The arguments to which the formal argumentas are mapped
+     * @param e The expression in which the substitution will take place
+     */
     def withParamSubst(realArgs: Seq[Expr], e: Expr) = {
       replaceFromIDs(paramSubst(realArgs), e)
     }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
index d49e3316716ae2277af5ea35c6115d076e7029bd..d52ac0704e65d119bf3f81c4a30d58723f9aea81 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
@@ -9,8 +9,6 @@ import purescala.Definitions._
 import purescala.Constructors._
 import purescala.ExprOps._
 
-import _root_.smtlib.parser.Commands.{Assert => _, FunDef => _, _}
-
 trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
 
   protected var currentFunDef: Option[FunDef] = None
@@ -30,14 +28,10 @@ trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
     val inductiveHyps = for {
       fi@FunctionInvocation(tfd, args) <- functionCallsOf(cond).toSeq
     } yield {
-      val formalToRealArgs = tfd.paramIds.zip(args).toMap
-      val post = tfd.postcondition map { post =>
-        application(
-          replaceFromIDs(formalToRealArgs, post),
-          Seq(fi)
-        )
-      } getOrElse BooleanLiteral(true)
-
+      val post = application(
+        tfd.withParamSubst(args, tfd.postOrTrue),
+        Seq(fi)
+      )
       and(tfd.precOrTrue, post)
     }