diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index eee37aa029fe6ad62ca5bf8b6566616d6739e574..2f96aa02ca15038aa6ec9cef6b3b86877397808a 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -57,7 +57,9 @@ object Definitions {
 
     def subDefinitions = Seq()
 
-    def toVariable : Variable = Variable(id, tpe)
+    // Warning: the variable will not have the same type as the ValDef, but 
+    // the Identifier type is enough for all use cases in Leon
+    def toVariable : Variable = Variable(id)
 
     setSubDefOwners()
   }
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 2792539aa51fc12eb6f2b7b09a6c120686085c97..059f2f00f7a50468bee1b78d93c9b58023e76cce 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -241,24 +241,8 @@ object Trees {
     val getType = BooleanType
   }
 
-  // tpe, if present, overrides the type of the underlying Identifier id.
-  // This is useful for variables that represent class fields with instantiated types.
-  // E.g. list.head when list: List[Int]
-  // @mk: TODO: This breaks symmetry with the rest of the trees and is ugly-ish.
-  //      Feel free to rename the underlying class and define constructor/extractor,
-  //      or do it some other way
-  class Variable(val id: Identifier, val tpe: Option[TypeTree]) extends Expr with Terminal {
-    val getType = tpe getOrElse id.getType
-    override def equals(that: Any) = that match {
-      case Variable(id2) => id == id2
-      case _ => false
-    }
-    override def hashCode: Int = id.hashCode
-  }
-
-  object Variable {
-    def apply(id: Identifier, tpe: Option[TypeTree] = None) = new Variable(id, tpe)
-    def unapply(v: Variable) = Some(v.id)
+  case class Variable(val id: Identifier) extends Expr with Terminal {
+    val getType = id.getType
   }
 
   /* Literals */
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 1d1c7e24d2f86e0adba4da6c810dbbf2a1ef3e36..513052d1e17025f1fe5dc805918b7d970c6719db 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -53,7 +53,7 @@ object ArrayTransformation extends TransformationPhase {
     }
     case v@Variable(i) => {
       val freshId = id2FreshId.get(i).getOrElse(i)
-      Variable(freshId, Some(v.getType))
+      Variable(freshId)
     }
 
     case LetVar(id, e, b) => {