diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index cfda320f7b8d14e69e68e87d68884eb95b7b851a..564216f21849855fccb329c4983d3658a9378f63 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -9,9 +9,7 @@ import purescala.Expressions._
 import purescala.ExprOps.{simplestValue, matchToIfThenElse}
 import purescala.Types._
 import purescala.Constructors._
-import purescala.TypeOps.instantiateType
 import purescala.Extractors._
-import utils._
 
 import cafebabe._
 import cafebabe.AbstractByteCodes._
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 273128e0a3f975c203e01ae3ea1d73b5d2574044..2d592e006baa855ac76ddf6c77ebd889d137d7fc 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -36,11 +36,10 @@ object Common {
 
     val getType = tpe
 
-    override def equals(other: Any): Boolean = {
-      if(other == null || !other.isInstanceOf[Identifier])
-        false
-      else
-        other.asInstanceOf[Identifier].globalId == this.globalId
+    override def equals(other: Any): Boolean = other match {
+      case null => false
+      case i: Identifier => i.globalId == this.globalId
+      case _ => false
     }
 
     override def hashCode: Int = globalId
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 960202301371a2226e034e8aa6f72e243aa5a883..a0e1e67af4063d36fede784a40b943175f096068 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -171,7 +171,7 @@ object Expressions {
     val subPatterns: Seq[Pattern]
     val binder: Option[Identifier]
 
-    private def subBinders = subPatterns.map(_.binders).foldLeft[Set[Identifier]](Set.empty)(_ ++ _)
+    private def subBinders = subPatterns.flatMap(_.binders).toSet
     def binders: Set[Identifier] = subBinders ++ binder.toSet
 
     def withBinder(b : Identifier) = { this match {
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 1ab85aed884aad3bf72b5cca65d9b0f8d532e726..7cf7aea4b35ff2c1451423c00b7eeec70e0a90a1 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -47,7 +47,7 @@ object MethodLifting extends TransformationPhase {
     case acd: AbstractClassDef =>
       val (r, c) = acd.knownChildren.map(makeCases(_, fdId, breakDown)).unzip
       val recs = r.flatten
-      val complete = c forall (x => x)
+      val complete = !(c contains false)
       if (complete) {
         // Children define all cases completely, we don't need to add anything
         (recs, true)
diff --git a/src/main/scala/leon/purescala/TypeOps.scala b/src/main/scala/leon/purescala/TypeOps.scala
index d1b99517312cfa305482e0a0cc47156523f4e1b5..49529c035fabc2b77e72f4dae001c507a0c9d7cb 100644
--- a/src/main/scala/leon/purescala/TypeOps.scala
+++ b/src/main/scala/leon/purescala/TypeOps.scala
@@ -12,14 +12,14 @@ import Constructors._
 
 object TypeOps {
   def typeDepth(t: TypeTree): Int = t match {
-    case NAryType(tps, builder) => 1+tps.foldLeft(0) { case (d, t) => d max typeDepth(t) }
+    case NAryType(tps, builder) => 1+ (0 +: (tps map typeDepth)).max
   }
 
   def typeParamsOf(t: TypeTree): Set[TypeParameter] = t match {
     case tp: TypeParameter => Set(tp)
     case _ =>
       val NAryType(subs, _) = t
-      subs.map(typeParamsOf).foldLeft(Set[TypeParameter]())(_ ++ _)
+      subs.flatMap(typeParamsOf).toSet
   }
 
   def canBeSubtypeOf(
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index e615fc373f22ce72e4d59b80518d40a6e5a625b5..297d92d2aefcd5b5ed18ddf22c139b2d1cde55a9 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -64,8 +64,8 @@ class SimpleTerminationChecker(context: LeonContext, program: Program) extends T
 
     // We check all functions that are in a "lower" scc. These must
     // terminate for all inputs in any case.
-    val sccLowerCallees = sccCallees.filterNot(_ == sccIndex)
-    val lowerDefs = sccLowerCallees.map(sccArray(_)).foldLeft(Set.empty[FunDef])(_ ++ _)
+    val sccLowerCallees = sccCallees - sccIndex
+    val lowerDefs = sccLowerCallees.flatMap(sccArray(_))
     val lowerOK = lowerDefs.forall(terminates(_).isGuaranteed)
     if (!lowerOK)
       return NoGuarantee
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index a9bd1c5c4d2dc2dbb9ee1ce8a8d035f6f3905c2f..329eaae06405b751b0e79e2c78a51a5897714b62 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -69,8 +69,7 @@ trait StructuralSize {
       }
     }
 
-    def caseClassType2MatchCase(_c: ClassType): MatchCase = {
-      val c = _c.asInstanceOf[CaseClassType] // required by leon framework
+    def caseClassType2MatchCase(c: CaseClassType): MatchCase = {
       val arguments = c.fields.map(vd => FreshIdentifier(vd.id.name, vd.getType))
       val argumentPatterns = arguments.map(id => WildcardPattern(Some(id)))
       val sizes = arguments.map(id => size(Variable(id)))
diff --git a/src/main/scala/leon/utils/Graphs.scala b/src/main/scala/leon/utils/Graphs.scala
index f3bc2b10028a705bca2fd78afb3fd456160ee711..604bef784df0cfbb4cabf04056676b27bd187089 100644
--- a/src/main/scala/leon/utils/Graphs.scala
+++ b/src/main/scala/leon/utils/Graphs.scala
@@ -203,7 +203,7 @@ object Graphs {
           if (outs(v2)) {
             true
           } else {
-            outs.map(rec).foldLeft(false)( _ || _ )
+            outs.map(rec).contains(true)
           }
         }
       }