diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index b8d259cd1821f33319e46b0067e5f552371c3a6a..20fccb748e466c20be6bdcf9e8c4e3c267d51dae 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -229,8 +229,8 @@ trait Expressions { self: Trees =>
     val subPatterns: Seq[Pattern]
     val binder: Option[ValDef]
 
-    private def subBinders = subPatterns.flatMap(_.binders).toSet
-    def binders: Set[ValDef] = subBinders ++ binder.toSet
+    private def subBinders = subPatterns.flatMap(_.binders)
+    def binders: Seq[ValDef] = binder.toSeq ++ subBinders
 
     def withBinder(b: ValDef) = { this match {
       case Pattern(None, subs, builder) => builder(Some(b), subs)
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index 050f9a48574c0e0d37d20d78b2a510c0626c2e5f..699874093161dd0526e0930b609163709698325d 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -299,7 +299,7 @@ trait Extractors { self: Trees =>
 
     def unapply(me: MatchExpr) : Option[(Pattern, Expr, Expr)] = {
       Option(me) collect {
-        case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliasedSymbols(pattern.binders, exprOps.variablesOf(scrut)) =>
+        case MatchExpr(scrut, List(SimpleCase(pattern, body))) if !aliasedSymbols(pattern.binders.toSet, exprOps.variablesOf(scrut)) =>
           ( pattern, scrut, body )
       }
     }