diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 2a4d6e077f3178cd3393bc71abfe4388ead2fa35..a6c202ba0c46f0b997bcb3230f8c17e1480a1871 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -48,25 +48,21 @@ trait ExprOps extends GenTreeOps {
     case _ => None
   } (expr)
 
-  protected class VariableExtractor {
-    def unapply(e: Expr): Option[(Set[Variable], Set[Variable])] = e match {
-      case v: Variable => Some((Set(v), Set.empty))
-      case Let(vd, _, _) => Some((Set.empty, Set(vd.toVariable)))
-      case Lambda(args, _) => Some((Set.empty, args.map(_.toVariable).toSet))
-      case Forall(args, _) => Some((Set.empty, args.map(_.toVariable).toSet))
-      case Choose(res, _) => Some((Set.empty, Set(res.toVariable)))
-      case _ => Some((Set.empty, Set.empty))
+  object VariableExtractor {
+    def unapply(e: Expr): Option[Set[Variable]] = {
+      val (vs, _, _, _) = deconstructor.deconstruct(e)
+      Some(vs.toSet)
     }
   }
 
-  protected val VariableExtractor = new VariableExtractor
-
   /** Returns the set of free variables in an expression */
   def variablesOf(expr: Expr): Set[Variable] = {
     fold[Set[Variable]] { case (e, subs) =>
       val subvs = subs.flatten.toSet
-      val VariableExtractor(add, remove) = e
-      subvs ++ add -- remove
+      e match {
+        case v: Variable => subvs + v
+        case VariableExtractor(vs) => subvs -- vs
+      }
     }(expr)
   }
 
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index a107bf1c4b1ad4e0b3468fb2f94e7ad00b33bed5..d7fcf07d62dc7188c591294ee9e1d1b0d320bf5e 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -72,11 +72,8 @@ trait Expressions { self: Trees =>
     */
   case class Let(vd: ValDef, value: Expr, body: Expr) extends Expr with CachingTyped {
     protected def computeType(implicit s: Symbols): Type = {
-      if (s.isSubtypeOf(value.getType, vd.tpe))
-        body.getType
-      else {
-        Untyped
-      }
+      if (s.isSubtypeOf(value.getType, vd.tpe)) body.getType
+      else Untyped
     }
   }