diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 8807b8761e93f5730e461806dd25423e8b493d0a..c7cc6a103c5d62a3ac523fe3a092edf6d6180833 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -709,11 +709,6 @@ trait CodeExtraction extends Extractors {
             val IntLiteral(ri) = rec(i)
             Waypoint(ri, rec(tree)).setType(pstpe)
           }
-          case ExSomeConstruction(tpe, arg) => {
-            // println("Got Some !" + tpe + ":" + arg)
-            val underlying = scalaType2PureScala(unit, silent)(tpe)
-            OptionSome(rec(arg)).setType(OptionType(underlying))
-          }
           case ExCaseClassConstruction(tpt, args) => {
             val cctype = scalaType2PureScala(unit, silent)(tpt.tpe)
             if(!cctype.isInstanceOf[CaseClassType]) {
@@ -1049,7 +1044,6 @@ trait CodeExtraction extends Extractors {
       case tpe if tpe == NothingClass.tpe => BottomType
       case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) => SetType(rec(btt))
       case TypeRef(_, sym, btt :: Nil) if isMultisetTraitSym(sym) => MultisetType(rec(btt))
-      case TypeRef(_, sym, btt :: Nil) if isOptionClassSym(sym) => OptionType(rec(btt))
       case TypeRef(_, sym, List(ftt,ttt)) if isMapTraitSym(sym) => MapType(rec(ftt),rec(ttt))
       case TypeRef(_, sym, List(t1,t2)) if isTuple2(sym) => TupleType(Seq(rec(t1),rec(t2)))
       case TypeRef(_, sym, List(t1,t2,t3)) if isTuple3(sym) => TupleType(Seq(rec(t1),rec(t2),rec(t3)))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7ab1b3c2f900b89a7e2c13267fb528da736489be..0f023bfb9ba5ca01d1209d3d76fa5ba8a0822103 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -114,16 +114,6 @@ object PrettyPrinter {
       nsb
     }
 
-    case OptionSome(a) => {
-      var nsb = sb
-      nsb.append("Some(")
-      nsb = pp(a, nsb, lvl)
-      nsb.append(")")
-      nsb
-    }
-
-    case OptionNone(_) => sb.append("None")
-
     case CaseClass(cd, args) => {
       var nsb = sb
       nsb.append(cd.id)
@@ -367,7 +357,6 @@ object PrettyPrinter {
     case SetType(bt) => pp(bt, sb.append("Set["), lvl).append("]")
     case MapType(ft,tt) => pp(tt, pp(ft, sb.append("Map["), lvl).append(","), lvl).append("]")
     case MultisetType(bt) => pp(bt, sb.append("Multiset["), lvl).append("]")
-    case OptionType(bt) => pp(bt, sb.append("Option["), lvl).append("]")
     case TupleType(tpes) => ppNaryType(sb, tpes, "(", ", ", ")", lvl)
     case c: ClassType => sb.append(c.classDef.id)
     case _ => sb.append("Type?")
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index b1cec54c57b6a920a26d4eb45360d3d085b728b3..aad213668f27a941a58219c8bc638f487f24cd38 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -114,14 +114,6 @@ object ScalaPrinter {
       sb.append("._" + i)
     }
 
-    case OptionSome(a) => {
-      sb.append("Some(")
-      pp(a, sb, lvl)
-      sb.append(")")
-    }
-
-    case OptionNone(_) => sb.append("None")
-
     case CaseClass(cd, args) => {
       sb.append(cd.id)
       ppNary(sb, args, "(", ", ", ")", lvl)
@@ -367,10 +359,6 @@ object ScalaPrinter {
       sb.append("Multiset[")
       pp(bt, sb, lvl)
       sb.append("]")
-    case OptionType(bt) =>
-      sb.append("Option[")
-      pp(bt, sb, lvl)
-      sb.append("]")
     case TupleType(tpes) => ppNaryType(sb, tpes, "(", ", ", ")", lvl)
     case c: ClassType => sb.append(c.classDef.id)
     case _ => sb.append("Type?")
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index e8516fc9a1607a7ead1d92ab6995a7542dd211fb..741b3fcaad2783b55b012ff9ac5479be5e92d98a 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -383,12 +383,6 @@ object Trees {
     val fixedType = BooleanType
   }
 
-  /* Option expressions */
-  case class OptionSome(value: Expr) extends Expr 
-  case class OptionNone(baseType: TypeTree) extends Expr with Terminal with FixedType {
-    val fixedType = OptionType(baseType)
-  }
-
   /* Set expressions */
   case class EmptySet(baseType: TypeTree) extends Expr with Terminal
   case class FiniteSet(elements: Seq[Expr]) extends Expr 
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 3e834e0b0dd38adc027241d06e79b598d3601b00..6dd49f7492c208e7aafd098f2b97236fa1874ef5 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -142,10 +142,6 @@ object TypeTrees {
       case (_,InfiniteSize) => InfiniteSize
       case (FiniteSize(n),FiniteSize(m)) => FiniteSize(scala.math.pow(m+1, n).toInt)
     }
-    case OptionType(base) => domainSize(base) match {
-      case InfiniteSize => InfiniteSize
-      case FiniteSize(n) => FiniteSize(n+1)
-    }
     case c: ClassType => InfiniteSize
   }
 
@@ -187,7 +183,6 @@ object TypeTrees {
   case class SetType(base: TypeTree) extends TypeTree
   case class MultisetType(base: TypeTree) extends TypeTree
   case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
-  case class OptionType(base: TypeTree) extends TypeTree
   case class ArrayType(base: TypeTree) extends TypeTree
 
   sealed abstract class ClassType extends TypeTree {
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index da6731a735697b85b0ee38287a4261c3b68a60ef..330bd00fc392d9afef2c235484b35e7cc5ce3228 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -75,7 +75,6 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
     case ListType(base) => sys.error("I don't know what to do")
     case TupleType(bases) => sys.error("I don't know what to do")
     case MapType(from, to) => sys.error("I don't know what to do")
-    case OptionType(base) => sys.error("I don't know what to do")
     case _ => sys.error("Unexpected type: " + t)
   }