diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 02510c7c8b10f26b3924c49d9a1f5d1715c9009f..98cc822d8cc4d3a2e7c34f2f23a23d8230eca256 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -2142,9 +2142,10 @@ object ExprOps extends GenTreeOps[Expr] {
     case _ =>
       fun
   }
-  var msgs: String = ""
-  implicit class BooleanAdder(b: Boolean) {
-    def <(msg: String) = {if(!b) msgs += msg; b}
+  
+  // Use this only to debug isValueOfType
+  private implicit class BooleanAdder(b: Boolean) {
+    @inline def <(msg: String) = {/*if(!b) println(msg); */b}
   }
 
   /** Returns true if expr is a value of type t */
@@ -2181,11 +2182,12 @@ object ExprOps extends GenTreeOps[Expr] {
         (ct == ct2) <  s"$ct not equal to $ct2" &&
         ((args zip ct.fieldsTypes) forall (argstyped => isValueOfType(argstyped._1, argstyped._2)))
       case (FiniteLambda(mapping, default, tpe), exTpe@FunctionType(ins, out)) =>
+        variablesOf(e).isEmpty &&
         tpe == exTpe
       case (Lambda(valdefs, body), FunctionType(ins, out)) =>
         variablesOf(e).isEmpty &&
-        (valdefs zip ins forall (vdin => (vdin._1.getType == vdin._2) < s"${vdin._1.getType} is not equal to ${vdin._2}")) &&
-        (body.getType == out) < s"${body.getType} is not equal to ${out}"
+        (valdefs zip ins forall (vdin => TypeOps.isSubtypeOf(vdin._2, vdin._1.getType) < s"${vdin._2} is not a subtype of ${vdin._1.getType}")) &&
+        (TypeOps.isSubtypeOf(body.getType, out)) < s"${body.getType} is not a subtype of ${out}"
       case (FiniteBag(elements, fbtpe), BagType(tpe)) =>
         fbtpe == tpe && elements.forall{ case (key, value) => isValueOfType(key, tpe) && isValueOfType(value, IntegerType) }
       case _ => false
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index 2488aec8cebdd6de10d070800a4991df2e9894ba..9212163a71956a25e23cce33b9c786fdffb4ccc3 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -109,12 +109,11 @@ class SelfPrettyPrinter {
       case _ => false
     } match {
       case None => orElse
-      case Some(l) =>
-        ctx.reporter.debug("Executing pretty printer for type " + v.getType + " : " + l + " on " + v)
+      case Some(Lambda(Seq(ValDef(id)), body)) =>
+        ctx.reporter.debug("Executing pretty printer for type " + v.getType + " : " + v + " on " + v)
         val ste = new DefaultEvaluator(ctx, program)
         try {
-          val toEvaluate = application(l, Seq(v))
-          val result = ste.eval(toEvaluate)
+          val result = ste.eval(body, Map(id -> v))
           
           result.result match {
             case Some(StringLiteral(res)) if res != "" =>