diff --git a/src/main/scala/inox/ast/CallGraph.scala b/src/main/scala/inox/ast/CallGraph.scala
index 11e39b1c7dbefe8f1fc6e51b45483181864f568e..5146be4a95f0489b7bddbf73ef764677f71aa103 100644
--- a/src/main/scala/inox/ast/CallGraph.scala
+++ b/src/main/scala/inox/ast/CallGraph.scala
@@ -9,7 +9,7 @@ trait CallGraph {
   private[ast] val trees: Trees
   import trees._
   import trees.exprOps._
-  val symbols: Symbols
+  protected val symbols: Symbols
 
   private def collectCallsInPats(fd: FunDef)(p: Pattern): Set[(FunDef, FunDef)] =
     (p match {
diff --git a/src/main/scala/inox/ast/Constructors.scala b/src/main/scala/inox/ast/Constructors.scala
index 4b6781e83adae1a8dce985cbf424f41b12b76388..9b11aad35d0673864951ffb1b8fc47c8740631e3 100644
--- a/src/main/scala/inox/ast/Constructors.scala
+++ b/src/main/scala/inox/ast/Constructors.scala
@@ -13,7 +13,7 @@ trait Constructors {
   private[ast] val trees: Trees
   import trees._
   import trees.exprOps._
-  implicit val symbols: Symbols
+  protected implicit val symbols: Symbols
   import symbols._
 
   /** If `isTuple`:
diff --git a/src/main/scala/inox/ast/Definitions.scala b/src/main/scala/inox/ast/Definitions.scala
index b6d136c2cb1a8b0fe0333e1a3d8d35890ae88312..1b497884ac1ecf3efdcb7a9df033e06157a832f3 100644
--- a/src/main/scala/inox/ast/Definitions.scala
+++ b/src/main/scala/inox/ast/Definitions.scala
@@ -3,7 +3,6 @@
 package inox
 package ast
 
-import scala.reflect._
 import scala.collection.mutable.{Map => MutableMap}
 
 trait Definitions { self: Trees =>
@@ -88,7 +87,7 @@ trait Definitions { self: Trees =>
         with Paths {
 
     private[ast] val trees: self.type = self
-    val symbols: this.type = this
+    protected val symbols: this.type = this
 
     // @nv: this is a hack to reinject `this` into the set of implicits
     // in scope when using the pattern:
diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 889a31a190b70de955fc05475f462e3c58e28244..e7d14301d2322fc9cccfcfba9edb4142df0935b6 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -27,7 +27,6 @@ import utils._
 trait SymbolOps extends TreeOps { self: TypeOps =>
   import trees._
   import trees.exprOps._
-  val symbols: Symbols
   import symbols._
 
   /** Computes the negation of a boolean formula, with some simplifications. */
diff --git a/src/main/scala/inox/ast/TypeOps.scala b/src/main/scala/inox/ast/TypeOps.scala
index 44abc861a214db18619372c3436ab821c6e628c9..8724b6e0e2d031a4bbd4a213771a5dbe49be3a42 100644
--- a/src/main/scala/inox/ast/TypeOps.scala
+++ b/src/main/scala/inox/ast/TypeOps.scala
@@ -6,7 +6,7 @@ package ast
 trait TypeOps {
   private[ast] val trees: Trees
   import trees._
-  implicit val symbols: Symbols
+  protected implicit val symbols: Symbols
 
   object typeOps extends GenTreeOps {
     val trees: TypeOps.this.trees.type = TypeOps.this.trees