diff --git a/src/main/scala/inox/grammars/Aspects.scala b/src/main/scala/inox/grammars/Aspects.scala
index 027e423f59e34010814960332dad50219f5a94ea..7ef23f7b1d7d46962ff62daca8bba3c2347b3bcf 100644
--- a/src/main/scala/inox/grammars/Aspects.scala
+++ b/src/main/scala/inox/grammars/Aspects.scala
@@ -27,6 +27,6 @@ trait Aspects { self: GrammarsUniverse =>
   trait Aspect extends Printable {
     final type Production = ProductionRule[Label, Expr]
 
-    def applyTo(l: Label, ps: Seq[Production])(implicit ctx: InoxContext): Seq[Production]
+    def applyTo(l: Label, ps: Seq[Production]): Seq[Production]
   }
 }
diff --git a/src/main/scala/inox/grammars/BaseGrammars.scala b/src/main/scala/inox/grammars/BaseGrammars.scala
index f1d4559b61e852c2fccd04644a267df328d333b4..b5800c3334e69bd04af96a776d87b955db4f9973 100644
--- a/src/main/scala/inox/grammars/BaseGrammars.scala
+++ b/src/main/scala/inox/grammars/BaseGrammars.scala
@@ -15,7 +15,7 @@ trait BaseGrammars { self: GrammarsUniverse =>
     */
   case object BaseGrammar extends SimpleExpressionGrammar {
 
-    def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = t match {
+    def computeProductions(t: Type): Seq[Prod] = t match {
       case BooleanType =>
         List(
           terminal(BooleanLiteral(false), BooleanC),
diff --git a/src/main/scala/inox/grammars/ClosureGrammars.scala b/src/main/scala/inox/grammars/ClosureGrammars.scala
index 5695a724ffc44dbdecc22b1e795dad9a63e75d6f..cbf304ab5b434009b58c0c8f28cde92229b914c4 100644
--- a/src/main/scala/inox/grammars/ClosureGrammars.scala
+++ b/src/main/scala/inox/grammars/ClosureGrammars.scala
@@ -9,7 +9,7 @@ trait ClosureGrammars { self: GrammarsUniverse =>
   import symbols._
 
   case object Closures extends ExpressionGrammar {
-    def computeProductions(lab: Label)(implicit ctx: InoxContext): Seq[ProductionRule[Label, Expr]] = lab.getType match {
+    def computeProductions(lab: Label): Seq[ProductionRule[Label, Expr]] = lab.getType match {
       case FunctionType(argsTpes, ret) =>
         val args = argsTpes.zipWithIndex.map { case (tpe, i) =>
           ValDef(FreshIdentifier("a"+i), tpe)
diff --git a/src/main/scala/inox/grammars/ConstantGrammars.scala b/src/main/scala/inox/grammars/ConstantGrammars.scala
index 88aa7d5b06fda5f58d69521164e235ba67a6fc98..f4b33ade7c89750fa47aec0d77cb5c7aaaabd983 100644
--- a/src/main/scala/inox/grammars/ConstantGrammars.scala
+++ b/src/main/scala/inox/grammars/ConstantGrammars.scala
@@ -22,7 +22,7 @@ trait ConstantGrammars { self: GrammarsUniverse =>
       BooleanLiteral(false)
     )
 
-    def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = {
+    def computeProductions(t: Type): Seq[Prod] = {
       val literals = collect[Expr]{
         case IsTyped(l:Literal[_], `t`) => Set(l)
         case _ => Set()
diff --git a/src/main/scala/inox/grammars/ElementaryGrammars.scala b/src/main/scala/inox/grammars/ElementaryGrammars.scala
index d38b2956a6410e0f29f2c5729f81482ad894c557..520d29c6e4e1e45c66b7b175c4a62a725a7a74f8 100644
--- a/src/main/scala/inox/grammars/ElementaryGrammars.scala
+++ b/src/main/scala/inox/grammars/ElementaryGrammars.scala
@@ -9,7 +9,7 @@ trait ElementaryGrammars { self: GrammarsUniverse =>
 
   /** Generates one production rule for each expression in a sequence that has compatible type */
   case class OneOf(inputs: Seq[Expr]) extends SimpleExpressionGrammar {
-    def computeProductions(lab: Type)(implicit ctx: InoxContext): Seq[Prod] = {
+    def computeProductions(lab: Type): Seq[Prod] = {
       inputs.collect {
         case i if isSubtypeOf(i.getType, lab.getType) =>
           terminal(i)
@@ -23,13 +23,13 @@ trait ElementaryGrammars { self: GrammarsUniverse =>
       case g => Seq(g)
     }
 
-    def computeProductions(label: Label)(implicit ctx: InoxContext): Seq[ProductionRule[Label, Expr]] =
+    def computeProductions(label: Label): Seq[ProductionRule[Label, Expr]] =
       subGrammars.flatMap(_.computeProductions(label))
   }
 
   /** The empty expression grammar */
   case class Empty() extends ExpressionGrammar {
-    def computeProductions(l: Label)(implicit ctx: InoxContext) = Nil
+    def computeProductions(l: Label) = Nil
   }
 
 }
diff --git a/src/main/scala/inox/grammars/EqualityGrammars.scala b/src/main/scala/inox/grammars/EqualityGrammars.scala
index 45a031405c3e4537b87da3e118f880907542bbac..e5a7bc7297ac558d463d3192152643d94b8475ba 100644
--- a/src/main/scala/inox/grammars/EqualityGrammars.scala
+++ b/src/main/scala/inox/grammars/EqualityGrammars.scala
@@ -13,7 +13,7 @@ trait EqualityGrammars { self: GrammarsUniverse =>
     * @param types The set of types for which equalities will be generated
     */
   case class EqualityGrammar(types: Set[Type]) extends SimpleExpressionGrammar {
-    def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = t match {
+    def computeProductions(t: Type): Seq[Prod] = t match {
       case BooleanType =>
         types.toList map { tp =>
           nonTerminal(List(tp, tp), { case Seq(a, b) => equality(a, b) }, Equals)
diff --git a/src/main/scala/inox/grammars/ExpressionGrammars.scala b/src/main/scala/inox/grammars/ExpressionGrammars.scala
index 908a662a193019ecacad67376e08b3b2526fdf1f..36c44cd614ac291d3a7a5d624984b6860bc0f103 100644
--- a/src/main/scala/inox/grammars/ExpressionGrammars.scala
+++ b/src/main/scala/inox/grammars/ExpressionGrammars.scala
@@ -18,7 +18,7 @@ trait ExpressionGrammars { self: GrammarsUniverse =>
       * @param lab The nonterminal for which production rules will be generated
       * @note This is the cached version of [[computeProductions]]. Clients should use this method.
       */
-    final def getProductions(lab: Label)(implicit ctx: InoxContext) = {
+    final def getProductions(lab: Label) = {
       cache.getOrElse(lab, {
         val res = applyAspects(lab, computeProductions(lab))
         cache += lab -> res
@@ -31,7 +31,7 @@ trait ExpressionGrammars { self: GrammarsUniverse =>
       * @param lab The nonterminal for which production rules will be generated
       * @note Clients should use the cached version, [[getProductions]] instead
       */
-    def computeProductions(lab: Label)(implicit ctx: InoxContext): Seq[ProductionRule[Label, Expr]]
+    def computeProductions(lab: Label): Seq[ProductionRule[Label, Expr]]
 
     protected def applyAspects(lab: Label, ps: Seq[ProductionRule[Label, Expr]])(implicit ctx: InoxContext) = {
       lab.aspects.foldLeft(ps) {
@@ -44,7 +44,7 @@ trait ExpressionGrammars { self: GrammarsUniverse =>
     //  Union(Seq(this, that))
     //}
 
-    final def printProductions(printer: String => Unit)(implicit ctx: InoxContext) {
+    final def printProductions(printer: String => Unit) {
       def sorter(lp1: (Label, Seq[ProductionRule[Label, Expr]]), lp2: (Label, Seq[ProductionRule[Label, Expr]])): Boolean = {
         val l1 = lp1._1
         val l2 = lp2._1
diff --git a/src/main/scala/inox/grammars/FunctionCallsGrammars.scala b/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
index 52b2de1d1f66196f2d739578a5c58d964d936e8a..b798e360a0b4c98780beaf19eeec9d2e6c8994e9 100644
--- a/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
+++ b/src/main/scala/inox/grammars/FunctionCallsGrammars.scala
@@ -16,7 +16,7 @@ trait FunctionCallsGrammars extends utils.Helpers { self: GrammarsUniverse =>
     * @param exclude An additional set of functions for which no calls will be generated
     */
   case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[Type], exclude: Set[FunDef]) extends SimpleExpressionGrammar {
-    def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = {
+    def computeProductions(t: Type): Seq[Prod] = {
 
       def getCandidates(fd: FunDef): Seq[TypedFunDef] = {
         // Prevents recursive calls
diff --git a/src/main/scala/inox/grammars/SimpleExpressionGrammars.scala b/src/main/scala/inox/grammars/SimpleExpressionGrammars.scala
index b571a32548b2c4035770d381892657869b7bc3eb..6282c52542ca3cadd9c0a941c2a6fbe54d8dc9b2 100644
--- a/src/main/scala/inox/grammars/SimpleExpressionGrammars.scala
+++ b/src/main/scala/inox/grammars/SimpleExpressionGrammars.scala
@@ -25,20 +25,20 @@ trait SimpleExpressionGrammars { self: GrammarsUniverse =>
 
     def filter(f: Prod => Boolean) = {
       new SimpleExpressionGrammar {
-        def computeProductions(lab: Type)(implicit ctx: InoxContext) = {
+        def computeProductions(lab: Type) = {
           SimpleExpressionGrammar.this.computeProductions(lab).filter(f)
         }
       }
     }
 
     // Finalize this to depend only on the type of the label
-    final def computeProductions(lab: Label)(implicit ctx: InoxContext): Seq[ProductionRule[Label, Expr]] = {
+    final def computeProductions(lab: Label): Seq[ProductionRule[Label, Expr]] = {
       computeProductions(lab.getType).map { p =>
         ProductionRule(p.subTrees.map(Label(_)), p.builder, p.tag, p.cost)
       }
     }
 
     /** Version of [[ExpressionGrammar.computeProductions]] which depends only a [[Type]] */
-    def computeProductions(tpe: Type)(implicit ctx: InoxContext): Seq[Prod]
+    def computeProductions(tpe: Type): Seq[Prod]
   }
 }
diff --git a/src/main/scala/inox/grammars/ValueGrammars.scala b/src/main/scala/inox/grammars/ValueGrammars.scala
index ea38e87b6c0a37a7e169f8a6edc6f63e6d82728f..81055c3baa639e0a5410d7c3369bf7e72a9cf0ec 100644
--- a/src/main/scala/inox/grammars/ValueGrammars.scala
+++ b/src/main/scala/inox/grammars/ValueGrammars.scala
@@ -10,7 +10,7 @@ trait ValueGrammars { self: GrammarsUniverse =>
 
   /** A grammar of values (ground terms) */
   case object ValueGrammar extends SimpleExpressionGrammar {
-    def computeProductions(t: Type)(implicit ctx: InoxContext): Seq[Prod] = t match {
+    def computeProductions(t: Type): Seq[Prod] = t match {
       case BooleanType =>
         List(
           terminal(BooleanLiteral(true), One),
diff --git a/src/main/scala/inox/grammars/aspects/DepthBoundAspects.scala b/src/main/scala/inox/grammars/aspects/DepthBoundAspects.scala
index 82c35c28cba616ab5162403fcd8a57c7f17aee86..3f617782af59f8cd8a339303f0120716b6c914a9 100644
--- a/src/main/scala/inox/grammars/aspects/DepthBoundAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/DepthBoundAspects.scala
@@ -13,7 +13,7 @@ trait DepthBoundAspects { self: GrammarsUniverse =>
 
     def asString(implicit opts: PrinterOptions): String = s"D$depth"
 
-    def applyTo(l: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+    def applyTo(l: Label, ps: Seq[Production]) = {
       if (depth == 0) Nil
       else if (depth == 1) ps.filter(_.isTerminal)
       else {
diff --git a/src/main/scala/inox/grammars/aspects/ExtraTerminalsAspects.scala b/src/main/scala/inox/grammars/aspects/ExtraTerminalsAspects.scala
index a64294ae8858ad3fc460902fc04283f3c6a5f177..2090376987a0f593e0a3258eefcf83cbdc2ee489 100644
--- a/src/main/scala/inox/grammars/aspects/ExtraTerminalsAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/ExtraTerminalsAspects.scala
@@ -19,7 +19,7 @@ trait ExtraTerminalsAspects { self: GrammarsUniverse =>
       s.toList.map(_.asString(opts)).mkString("{", ",", "}")
     }
 
-    override def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+    override def applyTo(lab: Label, ps: Seq[Production]) = {
       super.applyTo(lab, ps) ++ {
         s.filter(e => isSubtypeOf(e.getType, lab.getType)).map { e =>
           ProductionRule[Label, Expr](Nil, { (es: Seq[Expr]) => e }, Top, formulaSize(e))
diff --git a/src/main/scala/inox/grammars/aspects/PersistentAspects.scala b/src/main/scala/inox/grammars/aspects/PersistentAspects.scala
index 6f35c218ba6bb7b57546b0dc083b843277dc0d07..ff54abec841b4a995fd0e758702585456a2fba6c 100644
--- a/src/main/scala/inox/grammars/aspects/PersistentAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/PersistentAspects.scala
@@ -20,7 +20,7 @@ trait PersistentAspects { self: GrammarsUniverse =>
    *   e + 1
    */
   abstract class PersistentAspect extends Aspect {
-    def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+    def applyTo(lab: Label, ps: Seq[Production]) = {
       ps.map { p =>
         p.copy(subTrees = p.subTrees.map(lab => lab.withAspect(this)))
       }
diff --git a/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala b/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
index abbbe29d75bdf77c8d3564d1870f6585bae4436d..f5ed9bd5c905a9c646af112ce6153108a71c6267 100644
--- a/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/SimilarToAspects.scala
@@ -28,7 +28,7 @@ trait SimilarToAspects { self: GrammarsUniverse =>
      *                f(a, ~b~)
      *                f(b, a)   // if non-commut
      */
-    def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+    def applyTo(lab: Label, ps: Seq[Production]) = {
       def isCommutative(e: Expr) = e match {
         case _: EPlus | _: ETimes => true
         case _ => false
diff --git a/src/main/scala/inox/grammars/aspects/SizeAspects.scala b/src/main/scala/inox/grammars/aspects/SizeAspects.scala
index 2d39d2feeed3b0237e38838b6b9ad463894ff84b..911b79798739d6a5faa06883a72eb2d6bc0b84f3 100644
--- a/src/main/scala/inox/grammars/aspects/SizeAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/SizeAspects.scala
@@ -15,7 +15,7 @@ trait SizeAspects { self: GrammarsUniverse =>
   case class Sized(size: Int) extends Aspect {
     def asString(implicit opts: PrinterOptions) = "|"+size+"|"
 
-    def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+    def applyTo(lab: Label, ps: Seq[Production]) = {
       val optimizeCommut = true
 
       ps.flatMap { p =>
diff --git a/src/main/scala/inox/grammars/aspects/TaggedAspects.scala b/src/main/scala/inox/grammars/aspects/TaggedAspects.scala
index ab97369384af02d0c493edd80635ab1afdfd047f..34126a2c5555a03af7fc5b6a61d3f626294febbf 100644
--- a/src/main/scala/inox/grammars/aspects/TaggedAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/TaggedAspects.scala
@@ -19,7 +19,7 @@ trait TaggedAspects { self: GrammarsUniverse =>
       */
     def asString(implicit opts: PrinterOptions): String = s"#$tag$cString@$pos"
 
-    def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+    def applyTo(lab: Label, ps: Seq[Production]) = {
 
       // Tags to avoid depending on parent aspect
       val excludedTags: Set[Tag] = (tag, pos) match {
diff --git a/src/main/scala/inox/grammars/aspects/TypeDepthBoundAspects.scala b/src/main/scala/inox/grammars/aspects/TypeDepthBoundAspects.scala
index 5338f213b45266be379d76d2ac2dd8d5b44ba474..c1fc410a4c2efd8a64e4a702e55dd33787d47e80 100644
--- a/src/main/scala/inox/grammars/aspects/TypeDepthBoundAspects.scala
+++ b/src/main/scala/inox/grammars/aspects/TypeDepthBoundAspects.scala
@@ -12,7 +12,7 @@ trait TypeDepthBoundAspects { self: GrammarsUniverse =>
   case class TypeDepthBound(bound: Int) extends PersistentAspect {
     override def asString(implicit opts: PrinterOptions): String = "" // This is just debug pollution to print
 
-    override def applyTo(lab: Label, ps: Seq[Production])(implicit ctx: InoxContext) = {
+    override def applyTo(lab: Label, ps: Seq[Production]) = {
       if (depth(lab.getType) > bound) Nil
       else super.applyTo(lab, ps)
     }