diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 9de0a2a0539e625c1117b8987129c02e6fa2d395..4265fbecdb1d26e585a63fa61b2ae727b3dc96d1 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -86,7 +86,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
       e(caller) match {
         case l@Lambda(params, body) =>
           val newArgs = args.map(e)
-          val mapping = l.substitutions(newArgs)
+          val mapping = l.paramSubst(newArgs)
           e(body)(rctx.withNewVars(mapping), gctx)
         case f =>
           throw EvalError("Cannot apply non-lambda function " + f)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 50740179a9a08bdc12ccb88eeb79dba93af5ff66..1809ba00e66815cf0aec252d91340693ec1964ff 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1730,7 +1730,7 @@ object ExprOps {
         case LetTuple(is, es, b) =>
           letTuple(is, es, apply(b, args))
         case l@Lambda(params, body) =>
-          l.withSubstitutions(args, body)
+          l.withParamSubst(args, body)
         case _ => Application(expr, args)
       }
 
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 4f6ce84337d8e3cba59f28d40638467700e91ea4..0d2a840a30c6cc1ca921ad45687a5d52c2fa0630 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -94,19 +94,19 @@ object Expressions {
     }
   }
 
-  case class Application(caller: Expr, args: Seq[Expr]) extends Expr {
-    require(caller.getType.isInstanceOf[FunctionType])
-    val getType = caller.getType.asInstanceOf[FunctionType].to
+  case class Application(callee: Expr, args: Seq[Expr]) extends Expr {
+    require(callee.getType.isInstanceOf[FunctionType])
+    val getType = callee.getType.asInstanceOf[FunctionType].to
   }
 
   case class Lambda(args: Seq[ValDef], body: Expr) extends Expr {
     val getType = FunctionType(args.map(_.getType), body.getType).unveilUntyped
-    def substitutions(realArgs: Seq[Expr]) = {
+    def paramSubst(realArgs: Seq[Expr]) = {
       require(realArgs.size == args.size)
       (args map { _.id } zip realArgs).toMap
     }
-    def withSubstitutions(realArgs: Seq[Expr], e: Expr) = {
-      replaceFromIDs(substitutions(realArgs), e)
+    def withParamSubst(realArgs: Seq[Expr], e: Expr) = {
+      replaceFromIDs(paramSubst(realArgs), e)
     }
   }
 
@@ -261,6 +261,7 @@ object Expressions {
     val value = ()
   }
 
+  /* Case classes */
   case class CaseClass(ct: CaseClassType, args: Seq[Expr]) extends Expr {
     val getType = ct
   }
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index f8a13009089ee6dc056b10bc3ed408025126c25c..e63dad484842575fb65e290d7692cf42b821b947 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -39,7 +39,7 @@ object MethodLifting extends TransformationPhase {
         }
         val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
 
-        val receiver = FreshIdentifier("this", recType).setPos(cd.id)
+        val receiver = FreshIdentifier("thiss", recType).setPos(cd.id)
 
         val nfd = new FunDef(id, ctParams ++ fd.tparams, retType, ValDef(receiver) +: fdParams)
         nfd.copyContentFrom(fd)
@@ -70,7 +70,7 @@ object MethodLifting extends TransformationPhase {
 
       // 4) Remove methods in classes
       for (cd <- u.definedClasses) {
-        cd.clearMethods
+        cd.clearMethods()
       }
 
       u.copy(defs = defs ++ newCompanions)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 20596de878bebb9e58cffe538bd8c20322e37203..2195cb1263c133e79abbb24b70898d813bb83d3b 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -178,16 +178,15 @@ trait RuleDSL {
   // pc corresponds to the pc to reach the point where the solution is used. It
   // will be used if the sub-solution has a non-true pre.
   def termWrap(f: Expr => Expr, pc: Expr = BooleanLiteral(true)): List[Solution] => Option[Solution] = {
-    (sols: List[Solution]) => sols match {
-      case List(s) =>
-        val pre = if (s.pre == BooleanLiteral(true)) {
-          BooleanLiteral(true)
-        } else {
-          and(pc, s.pre)
-        }
-
-        Some(Solution(pre, s.defs, f(s.term), s.isTrusted))
-      case _ => None
-    }
+    case List(s) =>
+      val pre = if (s.pre == BooleanLiteral(true)) {
+        BooleanLiteral(true)
+      } else {
+        and(pc, s.pre)
+      }
+
+      Some(Solution(pre, s.defs, f(s.term), s.isTrusted))
+    case _ => None
+
   }
 }