diff --git a/src/main/scala/leon/laziness/ClosurePreAsserter.scala b/src/main/scala/leon/laziness/ClosurePreAsserter.scala
index a55cbbc00e7747835a9751e9c9140c1ebd761188..18398850ca56ec07407bf24041802919a6dd4469 100644
--- a/src/main/scala/leon/laziness/ClosurePreAsserter.scala
+++ b/src/main/scala/leon/laziness/ClosurePreAsserter.scala
@@ -1,20 +1,15 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
 import invariant.util._
 import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.Extractors._
 import purescala.Types._
 import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
 import leon.invariant.util.ProgramUtil._
 import leon.invariant.util.PredicateUtil._
 import LazinessUtil._
diff --git a/src/main/scala/leon/laziness/FreeVariableFactory.scala b/src/main/scala/leon/laziness/FreeVariableFactory.scala
index 9e93edb5e92e7d8b49a2dbab7346260867d1bc17..441da84ba6844b3922456d2d63f45d600bcc05d4 100644
--- a/src/main/scala/leon/laziness/FreeVariableFactory.scala
+++ b/src/main/scala/leon/laziness/FreeVariableFactory.scala
@@ -1,31 +1,11 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
 import invariant.util._
-import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.DefOps._
-import purescala.Extractors._
 import purescala.Types._
-import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
-import LazinessUtil._
-import invariant.util.ProgramUtil._
 
 /**
  * A class that maintains a data type that can used to
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 60daeb0d3e9e52da177f40c5cab429459899fde9..37e14755fef862f030a073ad7fe1655b7d6c0e01 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -1,40 +1,13 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
 import invariant.util._
 import invariant.structure.FunctionUtils._
 import purescala.ScalaPrinter
-import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.DefOps._
-import purescala.Extractors._
-import purescala.Types._
-import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import leon.verification.VerificationPhase
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.solvers._
-import leon.solvers.z3._
-import leon.transformations._
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
 import LazinessUtil._
-import invariant.datastructure._
-import invariant.util.ProgramUtil._
-import purescala.Constructors._
-import leon.verification._
-import PredicateUtil._
-import leon.invariant.engine._
 import LazyVerificationPhase._
 import utils._
 import java.io.
diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala
index 903ef54e9959cc5165f2d3fdda4cedae8ad23186..f65c385ed4b13c2534c0c93ce2b946073a3aa986 100644
--- a/src/main/scala/leon/laziness/LazinessUtil.scala
+++ b/src/main/scala/leon/laziness/LazinessUtil.scala
@@ -1,30 +1,16 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
-import invariant.util._
-import invariant.structure.FunctionUtils._
 import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
-import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.Extractors._
 import purescala.Types._
-import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
 import java.io.File
 import java.io.FileWriter
 import java.io.BufferedWriter
 import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
-import purescala.PrinterOptions
 
 object LazinessUtil {
 
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index a47855f267eeabfe2d30587a3b0a7720a1372f27..58fa1674135b4b2f07aaf2b94f4a44b0715d1e7a 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -1,29 +1,15 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
 import invariant.util._
 import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.DefOps._
 import purescala.Extractors._
 import purescala.Types._
 import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
 import LazinessUtil._
 import ProgramUtil._
 import PredicateUtil._
diff --git a/src/main/scala/leon/laziness/LazyClosureFactory.scala b/src/main/scala/leon/laziness/LazyClosureFactory.scala
index faab5ef4dc21771530c319d80e53a55108f262af..1a69fa89dd438210969981f1cd452e4ac6ba90cf 100644
--- a/src/main/scala/leon/laziness/LazyClosureFactory.scala
+++ b/src/main/scala/leon/laziness/LazyClosureFactory.scala
@@ -1,29 +1,13 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
 import invariant.util._
-import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.DefOps._
-import purescala.Extractors._
 import purescala.Types._
 import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
 import LazinessUtil._
 
 //case class ClosureData(tpe: TypeTree, absDef: AbstractClassDef, caseClass: Seq[CaseClassDef])
diff --git a/src/main/scala/leon/laziness/LazyExpressionLifter.scala b/src/main/scala/leon/laziness/LazyExpressionLifter.scala
index 96683d6114b2d58344b1d091098a431962cd1cb2..545fb761e644bf46ca001e451be6c7309e24bab1 100644
--- a/src/main/scala/leon/laziness/LazyExpressionLifter.scala
+++ b/src/main/scala/leon/laziness/LazyExpressionLifter.scala
@@ -1,41 +1,18 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
 import invariant.util._
 import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.DefOps._
 import purescala.Extractors._
 import purescala.Types._
 import purescala.TypeOps._
 import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import leon.verification.VerificationPhase
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.solvers._
-import leon.solvers.z3._
-import leon.transformations._
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
 import LazinessUtil._
-import invariant.datastructure._
 import invariant.util.ProgramUtil._
-import purescala.Constructors._
-import leon.verification._
-import PredicateUtil._
-import leon.invariant.engine._
 import FreeVariableFactory._
 
 object LazyExpressionLifter {
diff --git a/src/main/scala/leon/laziness/LazyFunctionsManager.scala b/src/main/scala/leon/laziness/LazyFunctionsManager.scala
index b5197ac4ca2d5ec6dacdd9a320e51a6b5cdd5795..46220895e63bc872014283950cdbeee854381f65 100644
--- a/src/main/scala/leon/laziness/LazyFunctionsManager.scala
+++ b/src/main/scala/leon/laziness/LazyFunctionsManager.scala
@@ -1,29 +1,11 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
 import invariant.util._
-import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
-import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.DefOps._
 import purescala.Extractors._
-import purescala.Types._
-import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
 import LazinessUtil._
 
 class LazyFunctionsManager(p: Program) {
diff --git a/src/main/scala/leon/laziness/LazyInstrumenter.scala b/src/main/scala/leon/laziness/LazyInstrumenter.scala
index 764a5606f74ab86edf11d6df81a07681519d6b87..6dc5a7e50f184daa34907ca12bc58e285539a318 100644
--- a/src/main/scala/leon/laziness/LazyInstrumenter.scala
+++ b/src/main/scala/leon/laziness/LazyInstrumenter.scala
@@ -1,28 +1,11 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
-import invariant.util._
-import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
-import purescala.ExprOps._
-import purescala.DefOps._
-import purescala.Extractors._
 import purescala.Types._
 import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
 import leon.transformations._
 import LazinessUtil._
 
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index dcc0384d73175de68d1c4984e594c275dbd3e99b..ed1a93c888e0594fc46aca946a17a929201aeb5b 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -1,40 +1,19 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
 import invariant.util._
 import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.DefOps._
-import purescala.Extractors._
-import purescala.Types._
-import leon.invariant.util.TypeUtil._
-import leon.invariant.util.LetTupleSimplification._
-import leon.verification.VerificationPhase
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.solvers._
-import leon.solvers.z3._
-import leon.transformations._
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
+import solvers._
+import transformations._
 import LazinessUtil._
-import invariant.datastructure._
-import invariant.util.ProgramUtil._
 import purescala.Constructors._
-import leon.verification._
+import verification._
 import PredicateUtil._
-import leon.invariant.engine._
+import invariant.engine._
 
 object LazyVerificationPhase {
 
diff --git a/src/main/scala/leon/laziness/TypeChecker.scala b/src/main/scala/leon/laziness/TypeChecker.scala
index 96687b85645037f2d5beb9e374f9397eda25c675..ab9c1b3e02a41b1a27c564b6ee845981ab8133d9 100644
--- a/src/main/scala/leon/laziness/TypeChecker.scala
+++ b/src/main/scala/leon/laziness/TypeChecker.scala
@@ -1,15 +1,13 @@
 package leon
 package laziness
 
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
-import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Types._
 import purescala.TypeOps._
-import leon.invariant.util.TypeUtil._
+import invariant.util.TypeUtil._
 
 object TypeChecker {
    /**
diff --git a/src/main/scala/leon/laziness/TypeRectifier.scala b/src/main/scala/leon/laziness/TypeRectifier.scala
index a048a969afd4fa9dcf091c5465494e2880bbc5a8..72d61bd7c33d8dcf6bcfc894dbde864921bd33f5 100644
--- a/src/main/scala/leon/laziness/TypeRectifier.scala
+++ b/src/main/scala/leon/laziness/TypeRectifier.scala
@@ -1,29 +1,15 @@
 package leon
 package laziness
 
-import invariant.factories._
-import invariant.util.Util._
-import invariant.util._
 import invariant.structure.FunctionUtils._
-import purescala.ScalaPrinter
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
-import purescala.DefOps._
 import purescala.Extractors._
 import purescala.Types._
 import leon.invariant.util.TypeUtil._
 import leon.invariant.util.LetTupleSimplification._
-import java.io.File
-import java.io.FileWriter
-import java.io.BufferedWriter
-import scala.util.matching.Regex
-import leon.purescala.PrettyPrinter
-import leon.LeonContext
-import leon.LeonOptionDef
-import leon.Main
-import leon.TransformationPhase
 import LazinessUtil._
 import leon.invariant.datastructure.DisjointSets
 import invariant.util.ProgramUtil._
@@ -34,14 +20,11 @@ import invariant.util.ProgramUtil._
  * Result is a program in which all type paramters of functions, types of
  * parameters of functions are correct.
  * The subsequent phase performs a local type inference.
- * @param placeHolderParameter Expected to returns true iff a type parameter
- * 														is meant as a placeholder and cannot be used
- * 														to represent a unified type
  */
 class TypeRectifier(p: Program, clFactory: LazyClosureFactory) {
 
   val typeClasses = {
-    var tc = new DisjointSets[TypeTree]()
+    val tc = new DisjointSets[TypeTree]()
     p.definedFunctions.foreach {
       case fd if fd.hasBody && !fd.isLibrary && !fd.isInvariant =>
         postTraversal {