diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 7dd3d3dd40585fdf24d7527fc4898f7339b88a82..9cfc6170a5c05e8faa6bca8cef7c6557ea39755d 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -5,11 +5,11 @@ package codegen
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps.{simplestValue, matchToIfThenElse}
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps.{simplestValue, matchToIfThenElse}
+import purescala.Types._
 import purescala.Constructors._
-import purescala.TypeTreeOps.instantiateType
+import purescala.TypeOps.instantiateType
 import purescala.Extractors._
 import utils._
 
@@ -555,7 +555,7 @@ trait CodeGeneration {
           CLASS_ACC_FINAL
         ).asInstanceOf[U2])
 
-        val closures = purescala.TreeOps.variablesOf(l).toSeq.sortBy(_.uniqueName)
+        val closures = purescala.ExprOps.variablesOf(l).toSeq.sortBy(_.uniqueName)
         val closureTypes = closures.map(id => id.name -> typeToJVM(id.getType))
 
         if (closureTypes.isEmpty) {
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 70f9342dd17380bc5191a577f5be872f183dcb8c..6fcdbc00f823a1a6b98301fb47ad3ce96fb4906f 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -5,8 +5,8 @@ package codegen
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Extractors._
 import purescala.Constructors._
 import codegen.runtime.LeonCodeGenRuntimeMonitor
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index e75c9b0bb9a709790f7b7d9d7cc3a3901d94a878..cdc6413ef4bdfac4751aebbddcf964c0340c2ada 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -4,7 +4,7 @@ package leon
 package codegen
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 import cafebabe._
 
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 0f8762d4eb605a9761cec88642b846eeb9aada24..d91b6e18d7ba59c6518b51fe3d3843cf45ad982e 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -6,9 +6,9 @@ package codegen.runtime
 import utils._
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees.{Tuple => LeonTuple, _}
-import purescala.TreeOps.valuateWithModel
-import purescala.TypeTrees._
+import purescala.Expressions.{Tuple => LeonTuple, _}
+import purescala.ExprOps.valuateWithModel
+import purescala.Types._
 import purescala.Constructors._
 import solvers.TimeoutSolver
 import solvers.z3._
diff --git a/src/main/scala/leon/codegen/runtime/GenericValues.scala b/src/main/scala/leon/codegen/runtime/GenericValues.scala
index 0bf7b27ae34efd56225e63c3442ac2fde567b392..685253d9ee0ddea80c700983702b78554035cf15 100644
--- a/src/main/scala/leon/codegen/runtime/GenericValues.scala
+++ b/src/main/scala/leon/codegen/runtime/GenericValues.scala
@@ -3,7 +3,7 @@
 package leon
 package codegen.runtime
 
-import purescala.Trees.GenericValue
+import purescala.Expressions.GenericValue
 import scala.collection.immutable.{Map => ScalaMap}
 
 object GenericValues {
diff --git a/src/main/scala/leon/datagen/DataGenerator.scala b/src/main/scala/leon/datagen/DataGenerator.scala
index 3a34af97f7cc4d7bfcb658795e8b219fc07a0c6c..555ed428ee08c44a5d4a46e0e12b0c783a7f9716 100644
--- a/src/main/scala/leon/datagen/DataGenerator.scala
+++ b/src/main/scala/leon/datagen/DataGenerator.scala
@@ -3,7 +3,7 @@
 package leon
 package datagen
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
 import utils._
 
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 91238109ab5e14f8ea80c72403ed345509f2f49f..70caf95cbcca752ec9b04be83030784987b8a7e5 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -4,8 +4,8 @@ package leon
 package datagen
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Definitions._
 import utils.StreamUtils._
 
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index daec365e46bc61d851c426bbd4ab7deaec912466..fac16d509df7dcc972255e0684970a405f76cd99 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -5,9 +5,9 @@ package datagen
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.TreeOps._
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index c21315468e5f948fcedc626eb4b597b25cfd4ea3..e097e75c10ece2a6b9c296a7a38dd8003bdbfdf3 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -5,7 +5,7 @@ package evaluators
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 
 import codegen.CompilationUnit
 import codegen.CodeGenParams
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index bf27ce8bd5105241226393468db3d3795f4322f9..66857a4f8214a6ad5a17314b6e6049e4da751ca5 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -4,7 +4,7 @@ package leon
 package evaluators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 
 class DefaultEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) {
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index bef203c064a75c68eab2c61e6ae47783af872850..f6f6a3cb03d9d68862bc79c6987de418d254623b 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -4,9 +4,9 @@ package leon
 package evaluators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
-import purescala.TypeTrees._
+import purescala.Types._
 
 import codegen._
 
diff --git a/src/main/scala/leon/evaluators/EvaluationResults.scala b/src/main/scala/leon/evaluators/EvaluationResults.scala
index caabd5f4cdf05434c839870bc7d448ed634bee87..8e6957f3f510ece6f0849bb9e7f35aaa96c18c29 100644
--- a/src/main/scala/leon/evaluators/EvaluationResults.scala
+++ b/src/main/scala/leon/evaluators/EvaluationResults.scala
@@ -3,7 +3,7 @@
 package leon
 package evaluators
 
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 
 object EvaluationResults {
   /** Possible results of expression evaluation. */
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 93c7129c4936d34cc931897a87632323f2677ae2..9c4403b1004663b6aecf1da8bd1bde4aa106641e 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -5,7 +5,7 @@ package evaluators
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 
 abstract class Evaluator(val context : LeonContext, val program : Program) extends LeonComponent {
 
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index e52d12904bcab37413283a273e1896cc9ce2a85c..e6e516c67021ac3311377c00fc5e085b234dbcad 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -5,9 +5,9 @@ package evaluators
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.TreeOps._
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Constructors._
 import purescala.Extractors._
 
@@ -504,7 +504,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
       e(impl)
 
     case choose @ Choose(_, None) =>
-      import purescala.TreeOps.simplestValue
+      import purescala.ExprOps.simplestValue
 
       implicit val debugSection = utils.DebugSectionSynthesis
 
@@ -571,7 +571,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
   }
 
   def matchesCase(scrut: Expr, caze: MatchCase)(implicit rctx: RC, gctx: GC): Option[(MatchCase, Map[Identifier, Expr])] = {
-    import purescala.TypeTreeOps.isSubtypeOf
+    import purescala.TypeOps.isSubtypeOf
 
     def matchesPattern(pat: Pattern, e: Expr): Option[Map[Identifier, Expr]] = (pat, e) match {
       case (InstanceOfPattern(ob, pct), CaseClass(ct, _)) =>
diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index 80757d88ab766031195e505ba5c634953988fd9c..39885c185b8c369ff2279d93214f1fdba46f069b 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -4,11 +4,11 @@ package leon
 package evaluators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Definitions._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) extends RecursiveEvaluator(ctx, prog, maxSteps) {
   type RC = TracingRecContext
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index cfcf667c56d25f8c33fd7b0b97326087fe116790..379413feae6ab50069f05c8afb1d32517cb40d01 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -17,13 +17,13 @@ import purescala.Definitions.{
   Import    => LeonImport,
   _
 }
-import purescala.Trees.{Expr => LeonExpr, This => LeonThis, _}
-import purescala.TypeTrees.{TypeTree => LeonType, _}
+import purescala.Expressions.{Expr => LeonExpr, This => LeonThis, _}
+import purescala.Types.{TypeTree => LeonType, _}
 import purescala.Common._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTreeOps._
+import purescala.ExprOps._
+import purescala.TypeOps._
 import purescala.DefOps.packageOf
 import xlang.Trees.{Block => LeonBlock, _}
 import xlang.TreeOps._
diff --git a/src/main/scala/leon/purescala/CallGraph.scala b/src/main/scala/leon/purescala/CallGraph.scala
index 77fa4cfa87f53f9c3493fcde2c11c8772f609736..38c6900204c0b0bbdea6fa377ffa5939f40b9cbc 100644
--- a/src/main/scala/leon/purescala/CallGraph.scala
+++ b/src/main/scala/leon/purescala/CallGraph.scala
@@ -4,8 +4,8 @@ package leon
 package purescala
 
 import Definitions._
-import Trees._
-import TreeOps._
+import Expressions._
+import ExprOps._
 
 class CallGraph(p: Program) {
 
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 7c6d32e04705dae3eaf2acd0be89e2b8517d6e49..6da84692bb895eccb0fa7e785f2a7fa8839dc8c7 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -7,8 +7,8 @@ import utils._
 import Definitions.Definition
 
 object Common {
-  import Trees.Variable
-  import TypeTrees._
+  import Expressions.Variable
+  import Types._
 
   abstract class Tree extends Positioned with Serializable {
     def copiedFrom(o: Tree): this.type = {
diff --git a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
index c3e2ba46cb3202f91ee03a191d42f48d1696a650..482bd06cffbd890a255d76a83630adcb941e85b0 100644
--- a/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
+++ b/src/main/scala/leon/purescala/CompleteAbstractDefinitions.scala
@@ -5,7 +5,7 @@ package purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 
 object CompleteAbstractDefinitions extends TransformationPhase {
 
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 3d316f8d8088b433239dfcd6e1f67b59e641970c..dcca26675e3a723946e4d7f6864a824f66d20151 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -4,12 +4,12 @@ package leon
 package purescala
 
 object Constructors {
-  import Trees._
-  import TreeOps._
+  import Expressions._
+  import ExprOps._
   import Definitions._
-  import TypeTreeOps._
+  import TypeOps._
   import Common._
-  import TypeTrees._
+  import Types._
 
   // If isTuple, the whole expression is returned. This is to avoid a situation
   // like tupleSelect(tupleWrap(Seq(Tuple(x,y))),1) -> x, which is not expected.
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 96acd8f225ffa827f7eaeecc992f58f46b75514c..25f5fb3848a5f8a26ae879dfb02a03bd15158d92 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -2,7 +2,7 @@ package leon.purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 
 object DefOps {
 
@@ -265,8 +265,8 @@ object DefOps {
   
   
   
-  import Trees.Expr
-  import TreeOps.{preMap, postMap}
+  import Expressions.Expr
+  import ExprOps.{preMap, postMap}
   
   /*
    * Apply an expression operation on all expressions contained in a FunDef
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 201835745eaf42538622d0b877cc770fc6d70e2b..680e7c0993f50ed7de08d71446b4f53547419c14 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -8,10 +8,10 @@ import utils.Library
 
 object Definitions {
   import Common._
-  import Trees._
-  import TreeOps._
-  import TypeTrees._
-  import TypeTreeOps._
+  import Expressions._
+  import ExprOps._
+  import Types._
+  import TypeOps._
 
   sealed abstract class Definition extends Tree {
     
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
similarity index 99%
rename from src/main/scala/leon/purescala/TreeOps.scala
rename to src/main/scala/leon/purescala/ExprOps.scala
index fe0a0c6ce5ef172618085ea44f92e4fab87a6926..2f7f2ab35a120be39f6bae7216edaae39f48e151 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -9,12 +9,12 @@ import leon.solvers._
 
 import scala.collection.concurrent.TrieMap
 
-object TreeOps {
+object ExprOps {
   import Common._
-  import TypeTrees._
+  import Types._
   import Definitions._
-  import Trees._
-  import TypeTreeOps._
+  import Expressions._
+  import TypeOps._
   import Extractors._
   import Constructors._
   import DefOps._
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Expressions.scala
similarity index 99%
rename from src/main/scala/leon/purescala/Trees.scala
rename to src/main/scala/leon/purescala/Expressions.scala
index 197fc891f882dd0e7d312642665557db9aee1946..32e56f1da9d27ec963ac833333ccfba8a0063422 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -6,10 +6,10 @@ package purescala
 import utils._
 
 /** AST definitions for Pure Scala. */
-object Trees {
+object Expressions {
   import Common._
-  import TypeTrees._
-  import TypeTreeOps._
+  import Types._
+  import TypeOps._
   import Definitions._
   import Extractors._
   import Constructors._
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 7077cf9f83227d0b3871f971efa86b31005d854c..9f705f388974c0fbb087ce37c71cfa129272f59e 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -3,16 +3,16 @@
 package leon
 package purescala
 
-import Trees._
+import Expressions._
 
 object Extractors {
   import Common._
-  import TypeTrees._
-  import TypeTreeOps._
+  import Types._
+  import TypeOps._
   import Definitions._
   import Extractors._
   import Constructors._
-  import TreeOps._
+  import ExprOps._
 
   object UnaryOperator {
     def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 7fcfb683e9ceb5a8ae3da4ba3038b31f0ffb272d..a9c443c4929fc7cff8d567e343706d4beaae1c1c 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -5,10 +5,10 @@ package purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 import Extractors._
-import TreeOps._
-import TypeTrees._
+import ExprOps._
+import Types._
 import Constructors._
 
 object FunctionClosure extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/FunctionMapping.scala b/src/main/scala/leon/purescala/FunctionMapping.scala
index c11c80a39b090d0c6825c76370ac5d37649e24da..a82b84f8395bc14db332f4c38fa622c5146fecc0 100644
--- a/src/main/scala/leon/purescala/FunctionMapping.scala
+++ b/src/main/scala/leon/purescala/FunctionMapping.scala
@@ -4,9 +4,9 @@ package leon
 package purescala
 
 import Definitions._
-import Trees._
-import TreeOps._
-import TypeTrees._
+import Expressions._
+import ExprOps._
+import Types._
 
 abstract class FunctionMapping extends TransformationPhase {
   
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index dc6ce8aea94635b7d68ce7c4eeee8b6086279789..6d970b65d867021ff162eff3fbae7b12f46285b8 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -5,11 +5,11 @@ package purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 import Extractors._
-import TreeOps._
-import TypeTrees._
-import TypeTreeOps.instantiateType
+import ExprOps._
+import Types._
+import TypeOps.instantiateType
 
 object MethodLifting extends TransformationPhase {
 
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index fd881faa5c86ba1ca1b18e2dd02b3e6b7f8d54fc..a54084b5f089045b3941938fd3bf8759e6840f3f 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -8,10 +8,10 @@ import leon.purescala.DefOps._
 import leon.purescala.Definitions._
 import leon.purescala.Extractors._
 import leon.purescala.PrinterHelpers._
-import leon.purescala.TreeOps.{isListLiteral, simplestValue}
-import leon.purescala.Trees._
-import leon.purescala.TypeTreeOps.leastUpperBound
-import leon.purescala.TypeTrees._
+import leon.purescala.ExprOps.{isListLiteral, simplestValue}
+import leon.purescala.Expressions._
+import leon.purescala.TypeOps.leastUpperBound
+import leon.purescala.Types._
 import leon.synthesis.Witnesses._
 
 case class PrinterContext(
diff --git a/src/main/scala/leon/purescala/RestoreMethods.scala b/src/main/scala/leon/purescala/RestoreMethods.scala
index e65add9c21fd696e7a5e446199443cfb4de9234b..353bb8697c8de6eba4746bd9394c5e129f3ac172 100644
--- a/src/main/scala/leon/purescala/RestoreMethods.scala
+++ b/src/main/scala/leon/purescala/RestoreMethods.scala
@@ -3,10 +3,10 @@ package leon.purescala
 import leon._
 import leon.purescala.Definitions._
 import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps.{replaceFromIDs,functionCallsOf}
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps.{replaceFromIDs,functionCallsOf}
 import leon.purescala.DefOps.{applyOnFunDef,preMapOnFunDef}
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import utils.GraphOps._
 
 object RestoreMethods extends TransformationPhase {
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index e38418c0a247f5200e244f53c80bc807cf10d681..45a3db6faac3c861b6efa3fb6d14a4a7e236d371 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -11,8 +11,8 @@ import PrinterHelpers._
 /** This pretty-printer only print valid scala syntax */
 class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) extends PrettyPrinter(opts, sb) {
   import Common._
-  import Trees._
-  import TypeTrees._
+  import Expressions._
+  import Types._
   import Definitions._
 
   import java.lang.StringBuffer
@@ -54,7 +54,7 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
       case SetCardinality(s)    => p"$s.size"
 
       case a@FiniteArray(elems, oDef, size) => {
-        import TreeOps._
+        import ExprOps._
         val ArrayType(underlying) = a.getType
         val default = oDef.getOrElse(simplestValue(underlying))
         size match {
diff --git a/src/main/scala/leon/purescala/ScopeSimplifier.scala b/src/main/scala/leon/purescala/ScopeSimplifier.scala
index 74cb530c762ccf69a3e0d4a16ae59d568b0a39cb..7a1299d68c29ef187bf37985a80619cdf0f1ef98 100644
--- a/src/main/scala/leon/purescala/ScopeSimplifier.scala
+++ b/src/main/scala/leon/purescala/ScopeSimplifier.scala
@@ -5,7 +5,7 @@ package purescala
 
 import Common._
 import Definitions._
-import Trees._
+import Expressions._
 import Extractors._
 
 class ScopeSimplifier extends Transformer {
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index 8cd319d891a6dd0dfdb6156072a4b08e41e41732..a3e1e02ec2adacf88ccfd5cdce093de65d372a43 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -3,9 +3,9 @@
 package leon
 package purescala
 
-import Trees._
-import TypeTrees._
-import TreeOps._
+import Expressions._
+import Types._
+import ExprOps._
 import Extractors._
 import Constructors._
 import solvers._
diff --git a/src/main/scala/leon/purescala/Transformer.scala b/src/main/scala/leon/purescala/Transformer.scala
index c623aa1dda491209bf54fe688782bc006eff77fb..46314714fb74038761b6ee96cd81d98b9270a72e 100644
--- a/src/main/scala/leon/purescala/Transformer.scala
+++ b/src/main/scala/leon/purescala/Transformer.scala
@@ -3,7 +3,7 @@
 package leon
 package purescala
 
-import purescala.Trees._
+import purescala.Expressions._
 
 
 trait Transformer {
diff --git a/src/main/scala/leon/purescala/TransformerWithPC.scala b/src/main/scala/leon/purescala/TransformerWithPC.scala
index 10cc17dfee933563c6ab4424eb93f7508dda3821..821f4c9ef7a83405782a802eced884212a67ef77 100644
--- a/src/main/scala/leon/purescala/TransformerWithPC.scala
+++ b/src/main/scala/leon/purescala/TransformerWithPC.scala
@@ -3,8 +3,8 @@
 package leon
 package purescala
 
-import Trees._
-import TreeOps._
+import Expressions._
+import ExprOps._
 import Extractors._
 import Constructors._
 
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 554d3268e2c7c771536f3d55a6a5bbdd26be6091..7b80083e498e882cbd899e282c4b444d0dd469d3 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -5,9 +5,9 @@ package purescala
 
 object TreeNormalizations {
   import Common._
-  import TypeTrees._
-  import Trees._
-  import TreeOps._
+  import Types._
+  import Expressions._
+  import ExprOps._
 
   /* TODO: we should add CNF and DNF at least */
 
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
similarity index 99%
rename from src/main/scala/leon/purescala/TypeTreeOps.scala
rename to src/main/scala/leon/purescala/TypeOps.scala
index dd6597e8fc5c26d4e82c691f93b60c9c854ef3e4..14eba4fe91daca7e24feb94f7692aaf8c538ebe2 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -3,15 +3,15 @@
 package leon
 package purescala
 
-import TreeOps.postMap
-import TypeTrees._
+import ExprOps.postMap
+import Types._
 import Definitions._
 import Common._
-import Trees._
+import Expressions._
 import Extractors._
 import Constructors._
 
-object TypeTreeOps {
+object TypeOps {
   def typeDepth(t: TypeTree): Int = t match {
     case NAryType(tps, builder) => 1+tps.foldLeft(0) { case (d, t) => d max typeDepth(t) }
   }
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/Types.scala
similarity index 98%
rename from src/main/scala/leon/purescala/TypeTrees.scala
rename to src/main/scala/leon/purescala/Types.scala
index 5119582455ba3ee6e91df4e7440099364366a286..091914350a5535775d76125df07d46712e6fbe30 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -5,11 +5,11 @@ package purescala
 
 import scala.language.implicitConversions
 
-object TypeTrees {
+object Types {
   import Common._
-  import Trees._
+  import Expressions._
   import Definitions._
-  import TypeTreeOps._
+  import TypeOps._
 
   trait Typed {
     def getType: TypeTree
diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala
index da65e5c1fa2c27400812149a1ca4274d20174d40..b521e8717e8be70999fc0f84248146a88ddbf386 100644
--- a/src/main/scala/leon/repair/RepairNDEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala
@@ -2,9 +2,9 @@ package leon.repair
 
 import leon.purescala._
 import Definitions._
-import Trees._
-import TypeTrees._
-import TreeOps.postMap
+import Expressions._
+import Types._
+import ExprOps.postMap
 import Constructors.not
 import leon.LeonContext
 import leon.evaluators.DefaultEvaluator
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 4446f786c608f7166f8eda9cf0313d6978aae033..75fe9e853548005a480cd6953ab11c9f29a064e0 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -3,8 +3,8 @@ package leon.repair
 import scala.collection.immutable.Map
 import scala.collection.mutable.{Map => MMap}
 import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 import leon.purescala.Definitions._
 import leon.LeonContext
 import leon.evaluators.RecursiveEvaluator
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 9e234643c7966db1923411b653113e92d12db199..0c2f298ee1051a7024dfa650d32935ffe1f08526 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -5,9 +5,9 @@ package repair
   
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.DefOps._
 import purescala.Constructors._
 import purescala.Extractors.unwrapTuple
diff --git a/src/main/scala/leon/repair/rules/GuidedCloser.scala b/src/main/scala/leon/repair/rules/GuidedCloser.scala
index 50b2557554cfa623bf64d753d38c0052bc7e132b..06f2508215a1b2daa388c9747e8919f97a894294 100644
--- a/src/main/scala/leon/repair/rules/GuidedCloser.scala
+++ b/src/main/scala/leon/repair/rules/GuidedCloser.scala
@@ -7,11 +7,11 @@ package rules
 import synthesis._
 
 import leon.utils.Simplifiers
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/repair/rules/GuidedDecomp.scala b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
index 2546dd4e5a595bbffb72c2d45f526b66ecf1fa51..bbac7dd0b940c8f4fcaf82142217f271705eb0ec 100644
--- a/src/main/scala/leon/repair/rules/GuidedDecomp.scala
+++ b/src/main/scala/leon/repair/rules/GuidedDecomp.scala
@@ -8,11 +8,11 @@ import synthesis._
 
 import leon.utils.Simplifiers
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/solvers/AssumptionSolver.scala b/src/main/scala/leon/solvers/AssumptionSolver.scala
index 73084bf6db15f5413b6e70f5ea8f61222ffa4766..f180eaf42605efef031c9c8db8a6b61f3c8fd3ba 100644
--- a/src/main/scala/leon/solvers/AssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/AssumptionSolver.scala
@@ -3,7 +3,7 @@
 package leon
 package solvers
 
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 
 trait AssumptionSolver extends Solver {
   def checkAssumptions(assumptions: Set[Expr]): Option[Boolean]
diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index 9ec495e88ef2b6dfcfd3764d79cedb271ba8fa12..5f158c79fd74e1b5ecd8bd036a87eacb455d8dce 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -7,10 +7,10 @@ import utils._
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 import datagen._
 
diff --git a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
index c888f38df1a447031059f11a7697773213125196..fb73f5f2918052bbbf2f02602ae59445d2c5a54e 100644
--- a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
@@ -6,11 +6,11 @@ package solvers
 import utils._
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 trait NaiveAssumptionSolver extends AssumptionSolver {
   self: IncrementalSolver =>
diff --git a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
index b8053b7658b26dc3dd37289c6c392dd4edcde623..e38c63e7f196318ce42069141c13e3fe1980a408 100644
--- a/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleAssumptionSolverAPI.scala
@@ -4,7 +4,7 @@ package leon
 package solvers
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 class SimpleAssumptionSolverAPI(sf: SolverFactory[AssumptionSolver]) extends SimpleSolverAPI(sf) {
 
diff --git a/src/main/scala/leon/solvers/SimpleSolverAPI.scala b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
index eafd3fbd32cb2e9898266d7b807f6e0534ce766e..325d5e1021e6907925657816ffec351f468765cd 100644
--- a/src/main/scala/leon/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
@@ -4,7 +4,7 @@ package leon
 package solvers
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 class SimpleSolverAPI(sf: SolverFactory[Solver]) {
   def solveVALID(expression: Expr): Option[Boolean] = {
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index e1b43034643b6ff64e70dbb9354bbcd6b6070e7d..9b278aeb6641ed7c40af0febabbda38dd784150a 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -4,7 +4,7 @@ package leon
 package solvers
 
 import utils._
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 import purescala.Common.Identifier
 
 
diff --git a/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala b/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
index 7fae46a9ca7a37de2ff2dda49a383fa680bee772..b6bcdc1f19abe515c1b3b941809119c17e290b02 100644
--- a/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutAssumptionSolver.scala
@@ -3,7 +3,7 @@
 package leon
 package solvers
 
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 
 trait TimeoutAssumptionSolver extends TimeoutSolver with AssumptionSolver {
 
diff --git a/src/main/scala/leon/solvers/combinators/DNFSolver.scala b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
index 0b06aeb966d1a0a030d03b78c0a8d5607ec499c0..d67b2094cf34c9f937a85f5ca9df6650356236e2 100644
--- a/src/main/scala/leon/solvers/combinators/DNFSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/DNFSolver.scala
@@ -6,8 +6,8 @@ package combinators
 
 import purescala.Common._
 import purescala.Constructors._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 class DNFSolver(val context: LeonContext,
                 underlyings: SolverFactory[Solver]) extends Solver {
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 4e9a28045aa84875087e65964050130831478ea5..b24617a4e7b20b52feb9bb6b14b56ad3af3ddfb0 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -5,7 +5,7 @@ package solvers
 package combinators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 import utils.Interruptible
 import scala.concurrent._
diff --git a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
index 5b089883b7a60cd08b27e8e6a61a18981bac1f1e..1230ac3c55bd55fb258bfad43e7b8618d550f000 100644
--- a/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/RewritingSolver.scala
@@ -5,7 +5,7 @@ package solvers
 package combinators
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 
 abstract class RewritingSolver[+S <: Solver, T](underlying: S) {
   val context = underlying.context
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 59ac92e7a11221bb02cacd51bfc75161311a5532..c2e9d7cfb9c0240ee8b5a5d32d84e584af5a3a00 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -7,8 +7,8 @@ package combinators
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 import solvers.templates._
 import utils.Interruptible
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 2f9e4423395dd7479949c887a1253d7099864bf8..366f977d203a07318487dadb05586a14e2693bbe 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -7,11 +7,11 @@ package smtlib
 import utils._
 import purescala._
 import Common._
-import Trees._
+import Expressions._
 import Extractors._
 import Constructors._
-import TypeTrees._
-import TreeOps.simplestValue
+import Types._
+import ExprOps.simplestValue
 
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
 import _root_.smtlib.parser.Commands._
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 4da09b251abfdda9f6855ff18fa0ac5a112308c5..30c1a967c1f5b19f9d34e6ab6bd2f18f48068479 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -7,10 +7,10 @@ package smtlib
 import utils._
 import purescala._
 import Common._
-import Trees._
+import Expressions._
 import Extractors._
-import TreeOps._
-import TypeTrees._
+import ExprOps._
+import Types._
 import Definitions._
 
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index fca07352c6c01236b1fa64eaa8f268f1bf0df4cc..6cb34c94b9505cf45e63f691fa6e8fc62abefe9c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -4,10 +4,10 @@ package smtlib
 
 import purescala._
 import Common._
-import Trees.{Assert => _, _}
+import Expressions.{Assert => _, _}
 import Extractors._
-import TreeOps._
-import TypeTrees._
+import ExprOps._
+import Types._
 import Constructors._
 import Definitions._
 import utils.IncrementalBijection
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 6c0e9cfbfd976274816e0dfae1bb813a641da2ef..376e99b6bedc452e89eb65025986abda20e78e6e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -7,10 +7,10 @@ package smtlib
 import utils._
 import purescala._
 import Common._
-import Trees._
+import Expressions._
 import Extractors._
-import TypeTrees._
-import TreeOps.simplestValue
+import Types._
+import ExprOps.simplestValue
 
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _}
 import _root_.smtlib.parser.Commands.{DefineSort, GetModel, DefineFun}
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index d8aa9026f49cbd7b9e58db2ee42d6c80e82698fe..6c69b458d7846d3d289f7f630b995dfdac85fdf7 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -5,9 +5,9 @@ package solvers
 package templates
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 
 class LambdaManager[T](encoder: TemplateEncoder[T]) {
   private type IdMap = Map[T, LambdaTemplate[T]]
diff --git a/src/main/scala/leon/solvers/templates/TemplateEncoder.scala b/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
index 7460ae0cf321d10f6d43f9d42092003dd56f5cef..829a40326be1dc1fb13147e44707b02d82bf109d 100644
--- a/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateEncoder.scala
@@ -5,7 +5,7 @@ package solvers
 package templates
 
 import purescala.Common.Identifier
-import purescala.Trees.Expr
+import purescala.Expressions.Expr
 
 trait TemplateEncoder[T] {
   def encodeId(id: Identifier): T
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 8a35871f491cacdec0cc6d8861196221bbfb7ddd..1ee5d303d8d93d39c3857992265ecad1c8aa124c 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -6,10 +6,10 @@ package templates
 
 import utils._
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/solvers/templates/TemplateInfo.scala b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
index 110e658a301c2805968124905d9137d8e267114c..0dce3f3246ce9530740e94bae3f36e04710c8de6 100644
--- a/src/main/scala/leon/solvers/templates/TemplateInfo.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateInfo.scala
@@ -5,7 +5,7 @@ package solvers
 package templates
 
 import purescala.Definitions.TypedFunDef
-import purescala.TypeTrees.TypeTree
+import purescala.Types.TypeTree
 
 case class TemplateCallInfo[T](tfd: TypedFunDef, args: Seq[T]) {
   override def toString = {
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index ddf513b8c5b01cc8bd131186342dfbe24c7ac357..74b453bc148c0a816949fa8c3bd14a758e2e5923 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -5,10 +5,10 @@ package solvers
 package templates
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 import evaluators._
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 015dc2ada44ddd862106990a8f16eee515389265..443b2f5ab4b84951457ee22a5f34cc4ade1f7f8c 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -6,10 +6,10 @@ package templates
 
 import utils._
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 import evaluators._
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 6237fde6a01ff5a1c14d73a2d6c2c8618a1d169d..529dabf2082ff31a09d1cfb2761fc29d7b0b5317 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -11,11 +11,11 @@ import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Extractors._
-import purescala.Trees._
-import purescala.TypeTreeOps._
+import purescala.Expressions._
+import purescala.TypeOps._
 import xlang.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 import scala.collection.mutable.{Map => MutableMap}
 import scala.collection.mutable.{Set => MutableSet}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index b9852dfe9fefe54576404d163793b57d7735e2dc..e111891c1c41c000ee879f7601b81d8ba574b514 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -10,11 +10,11 @@ import _root_.z3.scala._
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 import solvers.templates._
 
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 1ee010c4f71fef31cadc4fabcfc9c2f302c31fb1..aeaee81e0198da2ea0067d1875198fb6a3ffe84d 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -9,10 +9,10 @@ import leon.solvers._
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 
 /** This is a rather direct mapping to Z3, where all functions are left uninterpreted.
  *  It reports the results as follows (based on the negation of the formula):
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 5558c745ff5af705a582b13c08012a3edd2370b8..2532827ad21ac62cdaa1c845c82d8527c8a14faa 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -6,9 +6,9 @@ package solvers.z3
 import z3.scala._
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 
 trait Z3ModelReconstruction {
   self: AbstractZ3Solver =>
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 72ac87a52210ba779859ff14cc4171bac3b44dca..8e13922596a4505dcf8159f2dbaf5331063b6a59 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -5,8 +5,8 @@ package synthesis
 
 import purescala.Definitions._
 import purescala.Constructors._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import Witnesses._
 
 case class ChooseInfo(fd: FunDef,
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 7b2450facb0e0ef200b21e63ae5b2cd0d97021b0..ece2e85ce6242f1c3eef052e84159098a131e4db 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -4,9 +4,9 @@ package leon
 package synthesis
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/ConvertWithOracle.scala b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
index e35c6e58127835bbc476b68886c4e4b53918519c..9af1d42c772c1bbf408e4be367c04574a3dea0af 100644
--- a/src/main/scala/leon/synthesis/ConvertWithOracle.scala
+++ b/src/main/scala/leon/synthesis/ConvertWithOracle.scala
@@ -3,8 +3,8 @@
 package leon
 package synthesis
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index b6a0db402bd0796db54b1a33db7970b9661da23b..cf6575bd66ae716575ca35ddc03c535f1fb29239 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -5,8 +5,8 @@ package synthesis
 
 import graph._
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 abstract class CostModel(val name: String) {
   def solution(s: Solution): Cost
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 16edbd4ab05643bf350a6aa240e2b2e8b4023222..b1ce6099a2ff0895359f2c2635414116f303ab52 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -3,10 +3,10 @@
 package leon
 package synthesis
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
-import purescala.TreeOps._
-import purescala.TypeTrees.TypeTree
+import purescala.ExprOps._
+import purescala.Types.TypeTree
 import purescala.Common._
 import purescala.Constructors._
 import purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 11bd6e704a1216ceeef3d1de3ba7655057006991..d6dc34b2f55df9d94703327e0110c3399e7d21ed 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -3,7 +3,7 @@
 package leon
 package synthesis
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common.Tree
 import purescala.Definitions.Definition
 import purescala.ScalaPrinter
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index d3a7663e94dfbf9f1c3cd7e2385f8be2cdea1ca6..801748dd450cfe52ba0a4c560556f030586df436 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -3,7 +3,7 @@
 package leon
 package synthesis
 
-import purescala.Trees._
+import purescala.Expressions._
 import leon.utils.ASCIIHelpers._
 
 class Example(val ins: Seq[Expr])
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 684bae5c616591c2d8c6a4ef768687ce94b7ceb3..4a9314562068de5fcf0fadf833ce66a3c33323d7 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -4,9 +4,9 @@ package leon
 package synthesis
 
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.TreeNormalizations.linearArithmeticForm
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Common._
 import evaluators._
 
diff --git a/src/main/scala/leon/synthesis/PartialSolution.scala b/src/main/scala/leon/synthesis/PartialSolution.scala
index 187ec4d059086b17e684d4a1a63dd59dffcd733d..1f0bdaa47ac8a5fc8bd287e93733482656f174b1 100644
--- a/src/main/scala/leon/synthesis/PartialSolution.scala
+++ b/src/main/scala/leon/synthesis/PartialSolution.scala
@@ -3,7 +3,7 @@
 package leon
 package synthesis
 
-import purescala.Trees._
+import purescala.Expressions._
 
 import graph._
 
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 297b3210fde52ba4dc89d714743cd6242b7343aa..f1257f0913db2184f73502df7c928c0e2cb7065d 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -3,9 +3,9 @@
 package leon
 package synthesis
 
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 import leon.purescala.Common._
 import leon.purescala.Constructors._
 import leon.purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 90f3eb4ff546db143eb06d6222bed298ba98b1ac..e22367b8e5dd11887e59b1a0cc5babc51fe94d52 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -4,9 +4,9 @@ package leon
 package synthesis
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.ExprOps._
 import rules._
 
 abstract class Rule(val name: String) extends RuleDSL {
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 2eb1e73f1352ecb703f473451e2ad5916bce065f..91c6020eeb610432c12804b32ce32a4167f874ab 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -4,10 +4,10 @@ package leon
 package synthesis
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TypeTrees.{TypeTree,TupleType}
+import purescala.Expressions._
+import purescala.Types.{TypeTree,TupleType}
 import purescala.Definitions._
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 import leon.utils.Simplifiers
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index e59e1eaadacf9edd5f50c7a0f21f6c80796bfe62..3adc6f35183a99930d7c8a5edbd79099d77a5002 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -7,7 +7,7 @@ import solvers._
 import solvers.combinators.PortfolioSolverSynth
 import solvers.z3._
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions.{Program, FunDef}
 import purescala.Common.Identifier
 
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index de1916639622a7a5b009ccf46476821f0ca31532..0da2b6c81aa475056e036465274deeaf13c1bb87 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -2,7 +2,7 @@
 package leon
 package synthesis
 
-import purescala.TreeOps._
+import purescala.ExprOps._
 
 import purescala.ScalaPrinter
 import purescala.Definitions.{Program, FunDef}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 44246404e9f35f0080c39975444ee45e2514ce45..ee234633f3b06ffe96391a13c68580a6568cab03 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -5,11 +5,11 @@ package synthesis
 
 import purescala.Common._
 import purescala.Definitions.{Program, FunDef, ModuleDef, DefType, ValDef}
-import purescala.TreeOps._
-import purescala.Trees._
+import purescala.ExprOps._
+import purescala.Expressions._
 import purescala.Constructors._
 import purescala.ScalaPrinter
-import purescala.TypeTrees._
+import purescala.Types._
 import solvers._
 import solvers.combinators._
 import solvers.z3._
diff --git a/src/main/scala/leon/synthesis/Witnesses.scala b/src/main/scala/leon/synthesis/Witnesses.scala
index 1c454f09b5744784ba658f14f58604d9fab4180c..4633f3271353a76010c082212e305d29104fc3f5 100644
--- a/src/main/scala/leon/synthesis/Witnesses.scala
+++ b/src/main/scala/leon/synthesis/Witnesses.scala
@@ -1,10 +1,10 @@
 package leon.synthesis
 
 import leon.purescala._
-import TypeTrees._
+import Types._
 import Definitions.TypedFunDef
 import Extractors._
-import Trees.Expr
+import Expressions.Expr
 
 
 object Witnesses {
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 5bb9d6f5d8b70649d8f1e606cacd08ed460921a0..d27cbe9bc028ec98d23645f7f4c6ebd4f1cc9b54 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/ADTInduction.scala b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
index 73aa69f7a4e6c9fc2a4aeab3726b5017d45d03ae..e993c73dd3a4641a815205e3feccc3cb70ca7a51 100644
--- a/src/main/scala/leon/synthesis/rules/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTInduction.scala
@@ -6,11 +6,11 @@ package rules
 
 import solvers._
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 case object ADTInduction extends Rule("ADT Induction") {
diff --git a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
index 6c12864c5f41b5afe186975a6f4fc4494f5a0a70..2c0817ce1dbd0fe43231f8d7a5aab41aa438585e 100644
--- a/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTLongInduction.scala
@@ -6,11 +6,11 @@ package rules
 
 import solvers._
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 case object ADTLongInduction extends Rule("ADT Long Induction") {
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index a836f884322556380bdf0134ad9522d6785a83be..5f5fed010158cef53fe283b80a3d67786f740fb7 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -4,10 +4,10 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 import purescala.Definitions._
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 4d6dcca5c9c8786a1d266acdef0fb8bc1b4742f4..dc2a06e4d5ec6a0d3fdce0989e53166d73a88895 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 46fd17233ac07d0df0fa5cf610392913063c0da6..51e63ec0d879cac095e280fba4c7b146142394e6 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -4,9 +4,9 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Constructors._
 import evaluators._
 import codegen.CodeGenParams
diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala
index 4cf48c204279c34277f6c98bb04e07a1a9006554..d594d22c42405026096db7cd005b439814311f76 100644
--- a/src/main/scala/leon/synthesis/rules/CEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGIS.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TypeTrees._
+import purescala.Types._
 
 import utils._
 
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index f3191fdfce3346187be49e7089bc5153013ecf46..e4c2c1ad19690f445ef7c2523c37b3fad97ddf1c 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -9,13 +9,13 @@ import solvers._
 import solvers.z3._
 
 import verification._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
 import purescala.Definitions._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.TypeTreeOps._
+import purescala.TypeOps._
 import purescala.Extractors._
 import purescala.Constructors._
 import purescala.ScalaPrinter
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 203a35b7df3589d4658e5865c95beddf47cafc1a..905cdff751b7a2d1e313c7201f8dd154fd9c4ea0 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Constructors._
 
 case object CaseSplit extends Rule("Case-Split") {
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 71f4ea75580a8d8a68a5494faeb39b64d049ec2d..6b7e42599475f05459a72f60265957405fb4bac9 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -4,11 +4,11 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index b6e57333c9c86624b26ac8ea2a4b418b743eb827..d41bfb8dfb9e9c905df994ffc7c864f3fdc95abe 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -4,10 +4,10 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Common._
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Constructors._
 
 case object DetupleOutput extends Rule("Detuple Out") {
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 89da1b14d520c17b509b3133adcc2edcf034e786..e9946dccef0bc20095faac185bb3e5c3392b7e36 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index d331b492892a33ad08687f4d84584059b428ec32..977a3eb08e9f2198e67ff9e448204c8031d05804 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Constructors._
 
 import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index bb43d716b3fe03555c5bbf9cce227d3acbefd5c8..4add33594895fb9206e6fd42a7dcf6d9a0e76fe0 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -5,8 +5,8 @@ package synthesis
 package rules
 
 import leon.utils._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index a2a6f9955eefe6b673c3a06908d68fbb189fb115..17792cad82e6fbe62af2ec1864318b238305615c 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -5,8 +5,8 @@ package synthesis
 package rules
 
 import solvers._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 case object Ground extends Rule("Ground") {
diff --git a/src/main/scala/leon/synthesis/rules/IfSplit.scala b/src/main/scala/leon/synthesis/rules/IfSplit.scala
index ea115e42c17d5ccae1a37d6b821a46898c01dc7a..a29721e7e01cb954f3868c82abb9411f6ee3cc40 100644
--- a/src/main/scala/leon/synthesis/rules/IfSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/IfSplit.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 case object IfSplit extends Rule("If-Split") {
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 86ccb02adf9e582bd12a137c30aaf71bab142fe7..b0649e251aad55d206dad3c44714c64212cd8f48 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Constructors._
 
 import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
index 249c62f3084c4cd8bbd587f012b4f732827bf2fd..96f3de79dfe22aa38a4ef8d7b31120071cfdd31b 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -10,8 +10,8 @@ import solvers._
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 case object InlineHoles extends Rule("Inline-Holes") {
diff --git a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
index 47851103139cd63ba67b760c2d08822675046bbb..114fa697cfc48800ab3797f22164c030b91d0b78 100644
--- a/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InnerCaseSplit.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Constructors._
 
 case object InnerCaseSplit extends Rule("Inner-Case-Split"){
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala
index abf2545d56f708bdc50781c65341051ae4128e71..216ce8ad769329382122e9975144c141a6697f2e 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala
@@ -5,11 +5,11 @@ package synthesis
 package rules
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 
 case object IntInduction extends Rule("Int Induction") {
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index d943fb072ebabcd2bb470083dab6840d072f4dee..478d3fbd2562be62f5ba00552118ed4f5566a6c0 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -5,12 +5,12 @@ package synthesis
 package rules
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.TreeNormalizations._
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Definitions._
 import LinearEquations.elimVariable
 import evaluators._
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 69217a3369e5610b24b5006c4d2fc61ddc233549..3430bf8ab6ab718674682070c809f19d6d366f41 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -5,12 +5,12 @@ package synthesis
 package rules
 
 import purescala.Common._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.TreeNormalizations.linearArithmeticForm
 import purescala.TreeNormalizations.NonLinearExpressionException
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Constructors._
 import purescala.Definitions._
 import LinearEquations.elimVariable
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 5ad58a0a467da3941da81e64f279208c17222bc0..866fc3e02372967c81dc3bfc295392cd94da1ec7 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -5,8 +5,8 @@ package synthesis
 package rules
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 28256da4e9ea2c46b07074c73e00e99450da0996..56cc85223b56e472906857526caf88ab359807d8 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 import solvers._
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
index e329de9d16ced9fa07a334accfd84d53b97dbf28..08d9862ec3a5aa1add16d2adfcbc7a1d028eb2f1 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticInjection.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
index f1356c77d3493882441cae0c583a06d9455cd3cd..381d9cf2f484f81922595ac31ff92b74113d83ec 100644
--- a/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/rules/SelectiveInlining.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/TEGIS.scala b/src/main/scala/leon/synthesis/rules/TEGIS.scala
index 06bf87c601067623faae922a556e9bd23278f757..8aa44fe90d96d2435e62c8b98a702e58aa2c7670 100644
--- a/src/main/scala/leon/synthesis/rules/TEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGIS.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TypeTrees._
+import purescala.Types._
 import utils._
 
 case object TEGIS extends TEGISLike[TypeTree]("TEGIS") {
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 48ca570c2a6c86f54699f0947c3c4a4fad51e0ad..78fbd8a5b0f4397736501a0cf73e1bded31e49cf 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Constructors._
 
 import evaluators._
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 5311caf122d3ad02887f079f307e91c63928edd9..ee215e78fa25a4ae0be46f76b05a8cd401f4270e 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 3c304c1fdefeccb9c5cb73a27932df0ef81ab027..72c766ba43b5630c4f8fd97f2c79afc8da496815 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -4,8 +4,8 @@ package leon
 package synthesis
 package rules
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index 077003e82f9e13104164db13ce2e88c299924c6d..a2fc3150ad33ffc8dee4fe2a448c2489a0511dca 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -4,7 +4,7 @@ package leon
 package synthesis
 package rules
 
-import purescala.TreeOps._
+import purescala.ExprOps._
 
 case object UnusedInput extends NormalizingRule("UnusedInput") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index b2f5ced92cbade68ae90d05ca6f506ce266f092d..af474fb7e5dbbdf4b9a6cd7ac6e549edf0a1f6cd 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -6,13 +6,13 @@ import bonsai._
 
 import Helpers._
 
-import purescala.Trees.{Or => LeonOr, _}
+import purescala.Expressions.{Or => LeonOr, _}
 import purescala.Common._
 import purescala.Definitions._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.TypeTreeOps._
+import purescala.TypeOps._
 import purescala.Extractors._
 import purescala.ScalaPrinter
 import purescala.Constructors.finiteSet
diff --git a/src/main/scala/leon/synthesis/utils/Helpers.scala b/src/main/scala/leon/synthesis/utils/Helpers.scala
index 77634ff76e49b1ffa3616674c317d8267ed98fe9..cb73726c45df3ce2d3d9c0a55708c2e92e2f6a30 100644
--- a/src/main/scala/leon/synthesis/utils/Helpers.scala
+++ b/src/main/scala/leon/synthesis/utils/Helpers.scala
@@ -5,10 +5,10 @@ package synthesis
 package utils
 
 import purescala.Definitions._
-import purescala.TypeTrees._
+import purescala.Types._
 import purescala.Extractors._
-import purescala.TypeTreeOps._
-import purescala.Trees._
+import purescala.TypeOps._
+import purescala.Expressions._
 import purescala.DefOps._
 import purescala.Common._
 import Witnesses._
diff --git a/src/main/scala/leon/termination/ChainBuilder.scala b/src/main/scala/leon/termination/ChainBuilder.scala
index e73470f2a91239cec2edbd5f9ab113689e12e465..3718972884807ded519442067f963be40eedd787 100644
--- a/src/main/scala/leon/termination/ChainBuilder.scala
+++ b/src/main/scala/leon/termination/ChainBuilder.scala
@@ -4,11 +4,11 @@ package leon
 package termination
 
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 import leon.purescala.Constructors._
-import leon.purescala.TypeTreeOps._
+import leon.purescala.TypeOps._
 import leon.purescala.Common._
 
 import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 4a3e8270c4fe5f3d193269d4d09a2388968820ae..5f923fb0a5845f419ba6c6342c1c8d6c1039266c 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -3,10 +3,10 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
-import purescala.TypeTreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
+import purescala.TypeOps._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Common._
diff --git a/src/main/scala/leon/termination/ChainProcessor.scala b/src/main/scala/leon/termination/ChainProcessor.scala
index 817aec03d9f819c6fe0d61af9208ef4a98c90383..3bb3e17a096d616050e05b11c3286d49921d43d6 100644
--- a/src/main/scala/leon/termination/ChainProcessor.scala
+++ b/src/main/scala/leon/termination/ChainProcessor.scala
@@ -3,9 +3,9 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Common._
 import purescala.Extractors._
 import purescala.Definitions._
diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
index 127ff668128a73616d19af3401c17ecd9eed3dab..df603dfb8f7c7a693f1ae3e423dc7de0220c25aa 100644
--- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala
+++ b/src/main/scala/leon/termination/ComplexTerminationChecker.scala
@@ -4,7 +4,7 @@ package leon
 package termination
 
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 
 import scala.collection.mutable.{Map => MutableMap}
 
diff --git a/src/main/scala/leon/termination/LoopProcessor.scala b/src/main/scala/leon/termination/LoopProcessor.scala
index ec6bb2b89e4da31b58c6d6939e2a6ed6799cf457..4765a73c4daabe09010d12927563ea5d7106703c 100644
--- a/src/main/scala/leon/termination/LoopProcessor.scala
+++ b/src/main/scala/leon/termination/LoopProcessor.scala
@@ -5,8 +5,8 @@ package termination
 
 import purescala.Definitions._
 import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Constructors._
 
 import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index f4fe5c65e9547d7fbc7d654365a7f08c1161eb32..42cc27a2a89df581db500e635d895f981608ffa6 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -3,8 +3,8 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Common._
 import purescala.Definitions._
 
diff --git a/src/main/scala/leon/termination/RecursionProcessor.scala b/src/main/scala/leon/termination/RecursionProcessor.scala
index 89824297a36a1bae532bd441b9c60fe8c60ba939..210dfed177716db0a02c4cabbb0fce0913805a8b 100644
--- a/src/main/scala/leon/termination/RecursionProcessor.scala
+++ b/src/main/scala/leon/termination/RecursionProcessor.scala
@@ -3,7 +3,7 @@
 package leon
 package termination
 
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.Common._
 
 import scala.annotation.tailrec
diff --git a/src/main/scala/leon/termination/RelationBuilder.scala b/src/main/scala/leon/termination/RelationBuilder.scala
index c14a56a585efce8efdaa7143014f8d87f19dc732..018eca2e74070b529b8cf752b92a3b5392f1e4c4 100644
--- a/src/main/scala/leon/termination/RelationBuilder.scala
+++ b/src/main/scala/leon/termination/RelationBuilder.scala
@@ -3,8 +3,8 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Definitions._
 
 import scala.collection.mutable.{Map => MutableMap}
diff --git a/src/main/scala/leon/termination/RelationComparator.scala b/src/main/scala/leon/termination/RelationComparator.scala
index d50458d329bee652614bb888bca4471ea44bec33..7bb8fba698f462f0219063c40602ade1e67502a1 100644
--- a/src/main/scala/leon/termination/RelationComparator.scala
+++ b/src/main/scala/leon/termination/RelationComparator.scala
@@ -3,7 +3,7 @@
 package leon
 package termination
 
-import purescala.Trees._
+import purescala.Expressions._
 
 trait RelationComparator { self : StructuralSize =>
 
diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala
index 33f7c9da0d0aa7df5b36c27ac33dae53c4c5d9f9..1036a25bf9181112b5d5e30a603907a2222d954e 100644
--- a/src/main/scala/leon/termination/RelationProcessor.scala
+++ b/src/main/scala/leon/termination/RelationProcessor.scala
@@ -3,9 +3,9 @@
 package leon
 package termination
 
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 import leon.purescala.Common._
 import leon.purescala.Extractors._
 import leon.purescala.Constructors._
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index ada2df4a3cddb46e14711f283795bdcde65027f9..6ba21e23f9bcb8dc69ca973a83d0d1f634eac187 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -5,8 +5,8 @@ package termination
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 import scala.collection.mutable.{ Map => MutableMap }
 
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index d0f097d63bdeb5114fbfe364a90c61787256f757..d0c8bf1641d94fa35f041309202b97a11a1ad191 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -1,9 +1,9 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TypeTrees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.Types._
+import purescala.ExprOps._
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Constructors._
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 206e4ac444927a59b4d368ae7be2e4c3e9b70dde..8788a9496d6123a86e26aca6be4cd12438da018a 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -3,9 +3,9 @@
 package leon
 package termination
 
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Common._
diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala
index e4273dd852ea28638049284af5cb28c1da2cc14a..5a686f060be5bf324cfccc9e56a2346bf01d0dc6 100644
--- a/src/main/scala/leon/termination/TerminationChecker.scala
+++ b/src/main/scala/leon/termination/TerminationChecker.scala
@@ -4,7 +4,7 @@ package leon
 package termination
 
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import purescala.DefOps._
 
 abstract class TerminationChecker(val context: LeonContext, val program: Program) extends LeonComponent {
diff --git a/src/main/scala/leon/utils/GraphOps.scala b/src/main/scala/leon/utils/GraphOps.scala
index f7ad5646ac96ed11798a28366da7f8eee45cf590..b7d3adf92422eb0a0a008c17f765219c01302193 100644
--- a/src/main/scala/leon/utils/GraphOps.scala
+++ b/src/main/scala/leon/utils/GraphOps.scala
@@ -30,7 +30,7 @@ object GraphOps {
         graph.getOrElse(v, Set())
       }))
     }
-    leon.purescala.TreeOps.fixpoint(step, -1)(graph)
+    leon.purescala.ExprOps.fixpoint(step, -1)(graph)
   }
   
   def sources[A](graph : Map[A,Set[A]]) = {
diff --git a/src/main/scala/leon/utils/OracleTraverser.scala b/src/main/scala/leon/utils/OracleTraverser.scala
index 8c40f5f9eb2286d3319cc3672fbc770be4584c8b..3475a7a45d1d27f9c8d0fbb8317ee0c47d1faec0 100644
--- a/src/main/scala/leon/utils/OracleTraverser.scala
+++ b/src/main/scala/leon/utils/OracleTraverser.scala
@@ -3,8 +3,8 @@
 package leon
 package utils
 
-import purescala.Trees._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.Types._
 import purescala.Definitions._
 
 case class OracleTraverser(oracle: Expr, tpe: TypeTree, program: Program) {
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index 86d71130396bdd4297c033c0b8e10314f5c94bea..cd8cd8faaf0ee9adc2c00717e919e7a4b9c6361c 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -2,8 +2,8 @@ package leon
 package utils
 
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.ScopeSimplifier
 import solvers.z3.UninterpretedZ3Solver
 import solvers._
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 1b9b86f264c1d734b97007aa5b1cc087cf2cd75f..7c8d7c4c71b8605bbcd0b9d07404790cf6695e84 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -4,9 +4,9 @@ package leon
 package utils
 
 import purescala.Common._
-import purescala.TreeOps.preTraversal
-import purescala.TypeTrees._
-import purescala.Trees._
+import purescala.ExprOps.preTraversal
+import purescala.Types._
+import purescala.Expressions._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/utils/UnitElimination.scala b/src/main/scala/leon/utils/UnitElimination.scala
index 60f8bc232047c47900f728d817ac285d06f8482b..660f6e12324c06109f8728818978c2d08128ad2c 100644
--- a/src/main/scala/leon/utils/UnitElimination.scala
+++ b/src/main/scala/leon/utils/UnitElimination.scala
@@ -5,11 +5,11 @@ package utils
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
+import purescala.Expressions._
 import xlang.Trees._
 import purescala.Extractors._
 import purescala.Constructors._
-import purescala.TypeTrees._
+import purescala.Types._
 
 object UnitElimination extends TransformationPhase {
 
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 4d590e40aab5e6acb0b61e124710d4d902d2fe2e..c849441e092c48cdb66bc76d7d52eec434576fbc 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -5,9 +5,9 @@ package verification
 
 import purescala.Common._
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 
 import solvers._
 import solvers.z3._
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index e297bcd16df0021cece3f100917f0378777cb1dd..6ba584014fc813ce12b05b1147eaa1667ea113f8 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -3,8 +3,8 @@
 package leon
 package verification
 
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 9d7a7d8901631ad12d3716650f92bc3a18179739..b68abfa480731ee12dc7436f22ac6c4f1ba8f3af 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -4,9 +4,9 @@ package leon
 package verification
 
 import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.TypeTrees._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/verification/InjectAsserts.scala b/src/main/scala/leon/verification/InjectAsserts.scala
index 6844f776e38d68fa9027e4bab1104a1c46aedbad..cdeae613b36106909d3a0d160731c3365c243abb 100644
--- a/src/main/scala/leon/verification/InjectAsserts.scala
+++ b/src/main/scala/leon/verification/InjectAsserts.scala
@@ -3,9 +3,9 @@
 package leon
 package utils
 
-import purescala.Trees._
+import purescala.Expressions._
 import xlang.Trees._
-import purescala.TreeOps._
+import purescala.ExprOps._
 import purescala.Definitions._
 import purescala.Constructors._
 
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 8d80f5ffbfa0315f5a7b14175d3d38cfb0fdc7cf..92bf550b4397d08338c1701e50531240e759230e 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -4,8 +4,8 @@ package leon
 package verification
 
 import purescala.Definitions._
-import purescala.Trees._
-import purescala.TreeOps._
+import purescala.Expressions._
+import purescala.ExprOps._
 
 abstract class Tactic(vctx: VerificationContext) {
   val description : String
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index da53f8eacc7af4e7c0f10c04098a2026acb9dc0f..f0bb893ae670952d81f50a975e8778c05ccf2b03 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -2,7 +2,7 @@
 
 package leon.verification
 
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.Definitions._
 import leon.purescala.Common._
 import leon.utils.{Position, Positioned}
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 2f03dbaa417028e1e2e7bee36625eb1a05382c02..63a454ecc0b065f3a57c9c73d5d967b5e3a3d9bf 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -6,10 +6,10 @@ import leon.TransformationPhase
 import leon.LeonContext
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.xlang.Trees._
 import leon.purescala.Extractors._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 
 object ArrayTransformation extends TransformationPhase {
 
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 9828e45f0098cd8b485c93aa5212d4d1b3a03c4f..3a1c8498e8a33b54655ce199f726e72d672cb34a 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -6,8 +6,8 @@ import leon.TransformationPhase
 import leon.LeonContext
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
 import leon.xlang.Trees._
 
 object EpsilonElimination extends TransformationPhase {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 474d7a2b9d26527b44b865c27330ba085040633c..219acc60141cc5da8fc37904c2ee61178600260e 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -7,12 +7,12 @@ import leon.TransformationPhase
 import leon.LeonContext
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.Extractors._
 import leon.purescala.Constructors._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTreeOps._
+import leon.purescala.Types._
+import leon.purescala.ExprOps._
+import leon.purescala.TypeOps._
 import leon.xlang.Trees._
 
 object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef])] {
diff --git a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
index 8484b9840874376290c1391369becb585a13e9d4..38a42c494dccfddfd391bb6e220383c319069289 100644
--- a/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
+++ b/src/main/scala/leon/xlang/NoXLangFeaturesChecking.scala
@@ -3,7 +3,7 @@
 package leon
 package xlang
 
-import purescala.TreeOps.collect
+import purescala.ExprOps.collect
 import purescala.Definitions._
 
 import utils.Position
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index b76186d296a152a6eee0f57a1d0c7d7676e3c456..296bfe9f79ab7dc20646c63ad14bc170c7a962bc 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -3,9 +3,9 @@
 package leon
 package xlang
 
-import purescala.Trees._
+import purescala.Expressions._
 import xlang.Trees._
-import purescala.TreeOps._
+import purescala.ExprOps._
 
 object TreeOps {
   
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index e3d23d2cce5f557ab9e41048371bc00723fb9056..226e69c03423eaf0c49fc33e65dfaa1b3197edb3 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -4,8 +4,8 @@ package leon
 package xlang
 
 import purescala.Common._
-import purescala.TypeTrees._
-import purescala.Trees._
+import purescala.Types._
+import purescala.Expressions._
 import purescala.Extractors._
 import purescala.{PrettyPrintable, PrinterContext}
 import utils._
diff --git a/src/test/scala/leon/test/codegen/CodeGenTests.scala b/src/test/scala/leon/test/codegen/CodeGenTests.scala
index 607a6cd649b9cf42f2acc0d18a4d46517f2dee5a..ac17f0bda060483ac3a48693ce418f1e4cb025d9 100644
--- a/src/test/scala/leon/test/codegen/CodeGenTests.scala
+++ b/src/test/scala/leon/test/codegen/CodeGenTests.scala
@@ -5,8 +5,8 @@ package leon.test.codegen
 import leon._
 import leon.codegen._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 import leon.evaluators.{CodeGenEvaluator,EvaluationResults}
 import EvaluationResults._
 
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index dc79a820cf253fcd4eb7ad57cf5eb82788458528..9f3c7969fb79b641f9945a2a6e1b8afcc12cc352 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -10,9 +10,9 @@ import leon.frontends.scalac.ExtractionPhase
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.DefOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import leon.purescala.Constructors._
 
 class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index b0ea6159d9160f118fa55002b18c9c7593aaf993..2642dba5cbd5787bc6c4b6e4ac73a6d2f2374611 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -10,9 +10,9 @@ import leon.frontends.scalac.ExtractionPhase
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.DefOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import leon.purescala.Extractors._
 import leon.purescala.Constructors._
 
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index fd5afaef0c44fb4f2e10546b1ab491738ba3196b..45c7f066bb65b390d7b304673c1552d7ffc534ff 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -8,9 +8,9 @@ import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
 import leon.frontends.scalac.ExtractionPhase
 
 import leon.purescala.Common._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.Definitions._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import leon.datagen._
 
 import leon.evaluators._
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index dd72c6795ecf758aa8f0e1eb562dd64b6340be2e..36b802cca7b0eba1d10116b5aa4e99f89cbf3650 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -5,8 +5,8 @@ package leon.test.purescala
 import leon._
 import leon.test._
 import leon.purescala.Common._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 
 
 class LikelyEqSuite extends LeonTestSuite with WithLikelyEq {
diff --git a/src/test/scala/leon/test/purescala/TransformationTests.scala b/src/test/scala/leon/test/purescala/TransformationTests.scala
index 7335365aae0a0cd044e3ee5d895321a4f8877a14..e2c2bb7a836c7130c89ac8fc98d7ae6d9949bc10 100644
--- a/src/test/scala/leon/test/purescala/TransformationTests.scala
+++ b/src/test/scala/leon/test/purescala/TransformationTests.scala
@@ -10,9 +10,9 @@ import leon.frontends.scalac.ExtractionPhase
 import leon.purescala.ScalaPrinter
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 
 import leon.solvers.z3.UninterpretedZ3Solver
 import leon.solvers._
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index 61a7bbe9aa4d54c328aa93256403aa8aa6532420..f898dfee0b352b206b6d7dc724702311a2706495 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -7,9 +7,9 @@ import leon.test._
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.TypeTrees._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
+import leon.purescala.Types._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
 import leon.purescala.TreeNormalizations._
 
 class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 68e132d7ea9b26b740c7298b57c02e813ba39ba4..19ba9ae5dcc524424d862a5199a6b7ed2ee11bb9 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -9,9 +9,9 @@ import leon.LeonContext
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import leon.purescala.ExprOps._
 
 import leon.solvers.z3._
 
diff --git a/src/test/scala/leon/test/purescala/TreeTests.scala b/src/test/scala/leon/test/purescala/TreeTests.scala
index 1036fcd88fdfe75b49b840ce99e2e013f7083301..254441004b29e4f750d0ac6a833f31ab952f8c7a 100644
--- a/src/test/scala/leon/test/purescala/TreeTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeTests.scala
@@ -8,8 +8,8 @@ import leon.test._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Constructors._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 
 class TreeTests extends LeonTestSuite {
 
diff --git a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
index f784faea2fc5d90dcd47775e0e933c20827b3bbd..332777cd4ffa667c18d77400afc35e6f7f705d50 100644
--- a/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/EnumerationSolverTests.scala
@@ -9,8 +9,8 @@ import leon.solvers._
 import leon.solvers.combinators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 
 class EnumerationSolverTests extends LeonTestSuite {
   private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index cb8de56b308563f1f160e69dd16a474ece4a9554..8759d03ba5f614605417d0b0094aa795df116c6c 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -9,8 +9,8 @@ import leon.solvers._
 import leon.solvers.combinators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 
 class TimeoutSolverTests extends LeonTestSuite {
   private class IdioticSolver(val context : LeonContext, val program: Program) extends Solver with Interruptible{
diff --git a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
index 8fb31f28043198398d84a45854a289ab428d0dfa..0966c8b08e063123f1cdc7aca8b131f2c9f69b26 100644
--- a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
@@ -2,8 +2,8 @@ package leon.test.solvers
 
 import leon._
 import leon.test._
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.solvers._
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 901d1e05b6c93f0fd830e46b4b6c5751257b9969..e170dea4be5a7a0025799147a02e3ab71faee15d 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -5,9 +5,9 @@ package leon.test.solvers.z3
 import leon.test._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 
 import leon.solvers._
 import leon.solvers.z3._
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index e5816f5b13cd8d6d0bd9df1d4d4fce1a97daa1c1..ce7f9ce47aa31279be6cc6725d61d9aa4b05389f 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -5,9 +5,9 @@ package leon.test.solvers.z3
 import leon.test._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 
 import leon.solvers._
 import leon.solvers.z3._
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index cab51ede7c3184e2e98a68e66cc309ee6aadea9b..f9d6fc80ace052fd480f1ecd6a8d99078aed46d7 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -6,9 +6,9 @@ import leon.test._
 
 import leon.purescala.Common._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
-import leon.purescala.TypeTrees._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
+import leon.purescala.Types._
 
 import leon.solvers._
 import leon.solvers.z3._
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index dfa2b2ac77f4ff156ce1f8b427c4f96446e18588..46c35cb9ef75dc67fc4574ab2216d8c5e3501880 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -3,9 +3,9 @@
 package leon.test.synthesis
 import leon.test._
 
-import leon.purescala.Trees._
-import leon.purescala.TypeTrees._
-import leon.purescala.TreeOps._
+import leon.purescala.Expressions._
+import leon.purescala.Types._
+import leon.purescala.ExprOps._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.test.purescala.WithLikelyEq
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 16091cd8eb7cf881aec2db865f60e2519fd0632e..a1ffa10812feb8e5335af877e00086ffed85051a 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -5,8 +5,8 @@ import leon.test._
 
 import leon._
 import leon.purescala.Definitions._
-import leon.purescala.Trees._
-import leon.purescala.TreeOps._
+import leon.purescala.Expressions._
+import leon.purescala.ExprOps._
 import leon.solvers.z3._
 import leon.solvers.Solver
 import leon.synthesis._
diff --git a/src/test/scala/leon/test/utils/Streams.scala b/src/test/scala/leon/test/utils/Streams.scala
index e75af01ef08dc726897be657786f9bdbed8d2b65..dfca447258abc2396a58930b61a36f213d3808f7 100644
--- a/src/test/scala/leon/test/utils/Streams.scala
+++ b/src/test/scala/leon/test/utils/Streams.scala
@@ -8,9 +8,9 @@ import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
 import leon.frontends.scalac.ExtractionPhase
 
 import leon.purescala.Common._
-import leon.purescala.Trees._
+import leon.purescala.Expressions._
 import leon.purescala.Definitions._
-import leon.purescala.TypeTrees._
+import leon.purescala.Types._
 import leon.datagen._
 import leon.utils.StreamUtils._