diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index dd71afeec907abd4ed1b0df0a507750a857d544a..8e19f10081350fc71359bb1f601d5d53ecf67c0a 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -317,16 +317,21 @@ trait CodeExtraction extends Extractors {
 
 
     private def extractPattern(p: Tree, binder: Option[Identifier] = None): Pattern = p match {
-      case b @ Bind(name, Typed(pat, tpe)) =>
+      case b @ Bind(name, t @ Typed(pat, tpe)) =>
         val newID = FreshIdentifier(name.toString).setType(extractType(tpe.tpe))
         varSubsts(b.symbol) = (() => Variable(newID))
-        extractPattern(pat, Some(newID))
+        extractPattern(t, Some(newID))
 
       case b @ Bind(name, pat) =>
         val newID = FreshIdentifier(name.toString).setType(extractType(b.symbol.tpe))
         varSubsts(b.symbol) = (() => Variable(newID))
         extractPattern(pat, Some(newID))
 
+      case t @ Typed(Ident(nme.WILDCARD), tpe) if t.tpe.typeSymbol.isCase &&
+                                                  classesToClasses.contains(t.tpe.typeSymbol) =>
+        val cd = classesToClasses(t.tpe.typeSymbol).asInstanceOf[CaseClassDef]
+        InstanceOfPattern(binder, cd)
+
       case Ident(nme.WILDCARD) =>
         WildcardPattern(binder)
 
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 1d0cb59f391a5739acf27e3953dcba35721b2ca0..8371b8f0c852db4d9a0a6d2771b2d02eef36c7d6 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -691,7 +691,14 @@ object TreeOps {
     def rec(in: Expr, pattern: Pattern): Expr = {
       pattern match {
         case WildcardPattern(ob) => bind(ob, in)
-        case InstanceOfPattern(_,_) => scala.sys.error("InstanceOfPattern not yet supported.")
+        case InstanceOfPattern(ob, ct) =>
+          ct match {
+            case _: AbstractClassDef =>
+              bind(ob, in)
+
+            case cd: CaseClassDef =>
+              And(CaseClassInstanceOf(cd, in), bind(ob, in))
+          }
         case CaseClassPattern(ob, ccd, subps) => {
           assert(ccd.fields.size == subps.size)
           val pairs = ccd.fields.map(_.id).toList zip subps.toList