diff --git a/src/main/scala/inox/ast/SimpleSymbols.scala b/src/main/scala/inox/ast/SimpleSymbols.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e02d0f379871d01eb95d8ca84260bf5862a83de8
--- /dev/null
+++ b/src/main/scala/inox/ast/SimpleSymbols.scala
@@ -0,0 +1,36 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package ast
+
+trait SimpleSymbols { self: Trees =>
+
+  class Symbols(
+    val functions: Map[Identifier, FunDef],
+    val adts: Map[Identifier, ADTDefinition]
+  ) extends AbstractSymbols {
+
+    def transform(t: TreeTransformer) = new Symbols(
+      functions.mapValues(fd => new FunDef(
+        fd.id,
+        fd.tparams, // type parameters can't be transformed!
+        fd.params.map(vd => t.transform(vd)),
+        t.transform(fd.returnType),
+        t.transform(fd.fullBody),
+        fd.flags)),
+      adts.mapValues {
+        case sort: ADTSort => sort
+        case cons: ADTConstructor => new ADTConstructor(
+          cons.id,
+          cons.tparams,
+          cons.sort,
+          cons.fields.map(t.transform),
+          cons.flags)
+      })
+
+    def extend(functions: Seq[FunDef] = Seq.empty, adts: Seq[ADTDefinition] = Seq.empty) = new Symbols(
+      this.functions ++ functions.map(fd => fd.id -> fd),
+      this.adts ++ adts.map(cd => cd.id -> cd)
+    )
+  }
+}
diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index 9ae8863f52c1f22eeced0c52c11ccf111c477dff..755de6a1126e5ee076beab8c12f902477cb2fcbf 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -41,41 +41,10 @@ package object inox {
     }
   }
 
-  object trees extends ast.Trees {
-
+  object trees extends ast.Trees with ast.SimpleSymbols {
     object deconstructor extends {
       protected val s: trees.type = trees
       protected val t: trees.type = trees
     } with ast.TreeDeconstructor
-
-    class Symbols(
-      val functions: Map[Identifier, FunDef],
-      val adts: Map[Identifier, ADTDefinition]
-    ) extends AbstractSymbols {
-
-      def transform(t: TreeTransformer) = new Symbols(
-        functions.mapValues(fd => new FunDef(
-          fd.id,
-          fd.tparams, // type parameters can't be transformed!
-          fd.params.map(vd => t.transform(vd)),
-          t.transform(fd.returnType),
-          t.transform(fd.fullBody),
-          fd.flags)),
-        adts.mapValues {
-          case sort: ADTSort => sort
-          case cons: ADTConstructor => new ADTConstructor(
-            cons.id,
-            cons.tparams,
-            cons.sort,
-            cons.fields.map(t.transform),
-            cons.flags)
-        })
-
-      def extend(functions: Seq[FunDef] = Seq.empty, adts: Seq[ADTDefinition] = Seq.empty) = new Symbols(
-        this.functions ++ functions.map(fd => fd.id -> fd),
-        this.adts ++ adts.map(cd => cd.id -> cd)
-      )
-    }
-
   }
 }