diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b917447942ad3996163f5e970e316d0e1aee4b67..1d1b03ff9e5b3a680f4d952f8ecd7d9d9396686a 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -20,19 +20,19 @@ import scala.language.implicitConversions
   *
   * The generic operations lets you apply operations on a whole tree
   * expression. You can look at:
-  *   - [[SubTreeOps.fold foldRight]]
-  *   - [[SubTreeOps.preTraversal preTraversal]]
-  *   - [[SubTreeOps.postTraversal postTraversal]]
-  *   - [[SubTreeOps.preMap preMap]]
-  *   - [[SubTreeOps.postMap postMap]]
-  *   - [[SubTreeOps.genericTransform genericTransform]]
+  *   - [[GenTreeOps.fold foldRight]]
+  *   - [[GenTreeOps.preTraversal preTraversal]]
+  *   - [[GenTreeOps.postTraversal postTraversal]]
+  *   - [[GenTreeOps.preMap preMap]]
+  *   - [[GenTreeOps.postMap postMap]]
+  *   - [[GenTreeOps.genericTransform genericTransform]]
   *
   * These operations usually take a higher order function that gets applied to the
   * expression tree in some strategy. They provide an expressive way to build complex
   * operations on Leon expressions.
   *
   */
-object ExprOps extends { val Deconstructor = Operator } with SubTreeOps[Expr] {
+object ExprOps extends { val Deconstructor = Operator } with GenTreeOps[Expr] {
   /** Replaces bottom-up sub-identifiers by looking up for them in a map */
   def replaceFromIDs(substs: Map[Identifier, Expr], expr: Expr) : Expr = {
     postMap({
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index a975aa91a919b588649790c995639db4e6beb21c..7550b0304dd8b03d665b64e9e11ec6b9f2dd59bd 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -361,7 +361,7 @@ object Expressions {
   }
   
   // Extracts without taking care of the binder. (contrary to Extractos.Pattern)
-  object PatternExtractor extends SubTreeOps.Extractor[Pattern] {
+  object PatternExtractor extends TreeExtractor[Pattern] {
     def unapply(e: Pattern): Option[(Seq[Pattern], (Seq[Pattern]) => Pattern)] = e match {
       case (_: InstanceOfPattern) | (_: WildcardPattern) | (_: LiteralPattern[_]) =>
         Some(Seq(), es => e)
@@ -375,7 +375,9 @@ object Expressions {
     }
   }
   
-  object PatternOps extends { val Deconstructor = PatternExtractor } with SubTreeOps[Pattern]
+  object PatternOps extends GenTreeOps[Pattern] {
+    val Deconstructor = PatternExtractor
+  }
 
   /** Symbolic I/O examples as a match/case.
     * $encodingof `out == (in match { cases; case _ => out })`
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index ea5b30430005fecbb8eb6c5d8082a415cb1e24e2..304f242e7ed0cd814a506d309d80b26ed3a4a939 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -10,7 +10,7 @@ import Constructors._
 
 object Extractors {
 
-  object Operator extends SubTreeOps.Extractor[Expr] {
+  object Operator extends TreeExtractor[Expr] {
     def unapply(expr: Expr): Option[(Seq[Expr], (Seq[Expr]) => Expr)] = expr match {
       /* Unary operators */
       case Not(t) =>
diff --git a/src/main/scala/leon/purescala/SubTreeOps.scala b/src/main/scala/leon/purescala/GenTreeOps.scala
similarity index 97%
rename from src/main/scala/leon/purescala/SubTreeOps.scala
rename to src/main/scala/leon/purescala/GenTreeOps.scala
index 39ed1a45509648ed5bdc26b92f5006d815f8f941..bcf6002d156a8bb854bda077e17c5375b6cfaf50 100644
--- a/src/main/scala/leon/purescala/SubTreeOps.scala
+++ b/src/main/scala/leon/purescala/GenTreeOps.scala
@@ -6,13 +6,12 @@ package purescala
 import Common._
 import utils._
 
-object SubTreeOps {
-  trait Extractor[SubTree <: Tree] {
-    def unapply(e: SubTree): Option[(Seq[SubTree], (Seq[SubTree]) => SubTree)]
-  }
+trait TreeExtractor[SubTree <: Tree] {
+  def unapply(e: SubTree): Option[(Seq[SubTree], (Seq[SubTree]) => SubTree)]
 }
-trait SubTreeOps[SubTree <: Tree]  {
-  val Deconstructor: SubTreeOps.Extractor[SubTree]
+
+trait GenTreeOps[SubTree <: Tree]  {
+  val Deconstructor: TreeExtractor[SubTree]
   
   /* ========
    * Core API
@@ -208,7 +207,6 @@ trait SubTreeOps[SubTree <: Tree]  {
                       the current node
     * @param init the initial value
     * @param expr the expression on which to apply the transform
-    *
     * @see [[simpleTransform]]
     * @see [[simplePreTransform]]
     * @see [[simplePostTransform]]
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index 1a33a0883a1ec311126b6c165c542534c74dff9a..e0ba119b7a8299e45d32251fc794b53e3c07a4a8 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -10,7 +10,10 @@ import Expressions._
 import Extractors._
 import Constructors._
 
-object TypeOps extends { val Deconstructor = NAryType } with SubTreeOps[TypeTree] {
+object TypeOps extends GenTreeOps[TypeTree] {
+
+  val Deconstructor = NAryType
+
   def typeDepth(t: TypeTree): Int = t match {
     case NAryType(tps, builder) => 1 + (0 +: (tps map typeDepth)).max
   }
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 1536395e92798360c70b5ad8fcebf3520520768c..75693c375c717bcfe1b90074d635d663388ecb55 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -136,7 +136,7 @@ object Types {
   case class AbstractClassType(classDef: AbstractClassDef, tps: Seq[TypeTree]) extends ClassType
   case class CaseClassType(classDef: CaseClassDef, tps: Seq[TypeTree]) extends ClassType
 
-  object NAryType extends SubTreeOps.Extractor[TypeTree] {
+  object NAryType extends TreeExtractor[TypeTree] {
     def unapply(t: TypeTree): Option[(Seq[TypeTree], Seq[TypeTree] => TypeTree)] = t match {
       case CaseClassType(ccd, ts) => Some((ts, ts => CaseClassType(ccd, ts)))
       case AbstractClassType(acd, ts) => Some((ts, ts => AbstractClassType(acd, ts)))