diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 72623c96a2c732b4dac1995392545474c7f3f9c7..2cf52cd860700f284aecc27697c69cf8549974c1 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,6 +31,7 @@ object Main {
   }
 
   private def defaultAction(program: Program, reporter: Reporter) : Unit = {
+    println("Input program is:\n" + program)
     val passManager = new PassManager(Seq(ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
     val program2 = passManager.run(program)
     val analysis = new Analysis(program2, reporter)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index cbf4424bf7ad4d83ecb99f7a68302105b777f4d6..c418cdf4e4bb1f7fce36a2c8cce7ea1984855201 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -352,18 +352,16 @@ trait CodeExtraction extends Extractors {
         case a@Apply(fn, args) => {
           val pst = scalaType2PureScala(unit, silent)(a.tpe)
           pst match {
-            case TupleType(argsTpes) => {
-              println("Found tuple pattern match")
-              val patternIds: Seq[Identifier] = args.zipWithIndex.map{
-                case (b @ Bind(name, Ident(nme.WILDCARD)), i) => {
-                  val newID = FreshIdentifier(name.toString).setType(argsTpes(i))
-                  varSubsts(b.symbol) = (() => Variable(newID))
-                  newID
-                }
-                case _ => throw ImpureCodeEncounteredException(p)
-              }
-              TuplePattern(patternIds)
-            }
+            case TupleType(argsTpes) => TuplePattern(None, args.map(pat2pat))
+            case _ => throw ImpureCodeEncounteredException(p)
+          }
+        }
+        case b @ Bind(name, a @ Apply(fn, args)) => {
+          val newID = FreshIdentifier(name.toString).setType(scalaType2PureScala(unit,silent)(b.symbol.tpe))
+          varSubsts(b.symbol) = (() => Variable(newID))
+          val pst = scalaType2PureScala(unit, silent)(a.tpe)
+          pst match {
+            case TupleType(argsTpes) => TuplePattern(Some(newID), args.map(pat2pat))
             case _ => throw ImpureCodeEncounteredException(p)
           }
         }
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 9cc5b7b626a866430398cbd38a0faadb7b54cdee..6f2038edeab63f6a2dcc0809d4b912429f55b5eb 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -295,6 +295,16 @@ object PrettyPrinter {
         }
         case WildcardPattern(None)     => sb.append("_")
         case WildcardPattern(Some(id)) => sb.append(id)
+        case TuplePattern(bndr, subPatterns) => {
+          bndr.foreach(b => sb.append(b + " @ "))
+          sb.append("(")
+          subPatterns.init.foreach(p => {
+            ppc(sb, p)
+            sb.append(", ")
+          })
+          ppc(sb, subPatterns.last)
+          sb.append(")")
+        }
         case _ => sb.append("Pattern?")
       }
 
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index e738708a6c0c288039f85ff01dd17bfd99d82517..f44b09dd6bef8364e9eabd44d96656578a35bb76 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -144,10 +144,7 @@ object Trees {
   //   		      subPatterns: Seq[Pattern]) extends Pattern // c @ Extractor(...,...)
   // We don't handle Seq stars for now.
 
-  case class TuplePattern(elementsBinders: Seq[Identifier]) extends Pattern {
-    val binder = None
-    val subPatterns = Seq.empty
-  }
+  case class TuplePattern(binder: Option[Identifier], subPatterns: Seq[Pattern]) extends Pattern
 
   /* Propositional logic */
   object And {
@@ -1215,7 +1212,17 @@ object Trees {
           case None => together
         }
       }
-      case TuplePattern(ids) => ids.zipWithIndex.map{case (id, i) => (id, TupleSelect(in, i+1).setType(id.getType)) }.toMap
+      case TuplePattern(b, subps) => {
+        val TupleType(tpes) = in.getType
+        assert(tpes.size == subps.size)
+
+        val maps = subps.zipWithIndex.map{case (p, i) => mapForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
+        val map = maps.foldLeft(Map.empty[Identifier,Expr])(_ ++ _)
+        b match {
+          case Some(id) => map + (id -> in)
+          case None => map
+        }
+      }
     }
 
     def conditionForPattern(in: Expr, pattern: Pattern) : Expr = pattern match {
@@ -1228,7 +1235,12 @@ object Trees {
         val together = And(subTests)
         And(CaseClassInstanceOf(ccd, in), together)
       }
-      case TuplePattern(ids) => BooleanLiteral(true)
+      case TuplePattern(_, subps) => {
+        val TupleType(tpes) = in.getType
+        assert(tpes.size == subps.size)
+        val subTests = subps.zipWithIndex.map{case (p, i) => conditionForPattern(TupleSelect(in, i+1).setType(tpes(i)), p)}
+        And(subTests)
+      }
     }
 
     def rewritePM(e: Expr) : Option[Expr] = e match {