Revert "Fix treatment of 'this' in MethodLifting"

This reverts commit c4bf3e88.

src/main/scala/leon/purescala/MethodLifting.scala

@@ -79,8 +79,8 @@ object MethodLifting extends TransformationPhase {
         val at = acd.typed
         val binder = FreshIdentifier(acd.id.name.toLowerCase, at, true)
         def subst(e: Expr): Expr = e match {
-          case This(ct) =>
-            asInstOf(Variable(binder), ct)
+          case This(`at`) =>
+            Variable(binder)
           case e =>
             e
         }
@@ -158,19 +158,14 @@ object MethodLifting extends TransformationPhase {
         nfd.addFlag(IsMethod(cd))
 
         if (cd.knownDescendants.forall( cd => (cd.methods ++ cd.fields).forall(_.id != fd.id))) {
-          // Don't need to compose methods
           val paramsMap = fd.params.zip(fdParams).map{case (x,y) => (x.id, y.id)}.toMap
-          def thisToReceiver(e: Expr): Option[Expr] = e match {
-            case th@This(ct) => //if ct.classDef == cd =>
-              Some(asInstOf(receiver.toVariable, ct).setPos(th))
+          // Don't need to compose methods
+          nfd.fullBody = postMap {
+            case th@This(ct) if ct.classDef == cd =>
+              Some(receiver.toVariable.setPos(th))
             case _ =>
               None
-          }
-          nfd.fullBody = instantiateType(
-            postMap(thisToReceiver)(nfd.fullBody),
-            tparamsMap,
-            paramsMap
-          )
+          }(instantiateType(nfd.fullBody, tparamsMap, paramsMap))
         } else {
           // We need to compose methods of subclasses