diff --git a/src/main/scala/org/kframework/backend/skala/SkalaBackend.scala b/src/main/scala/org/kframework/backend/skala/SkalaBackend.scala
index d03e0e6..8a300ba 100644
--- a/src/main/scala/org/kframework/backend/skala/SkalaBackend.scala
+++ b/src/main/scala/org/kframework/backend/skala/SkalaBackend.scala
@@ -62,35 +62,7 @@ object Encodings {
 object Hook {
   def apply(s: kore.SymbolDeclaration)(implicit env: StandardEnvironment): Option[Label] = {
     s.att.getSymbolValue(Encodings.hook) match {
-      case Some(v) => v.str match {
-        case "INT.Int" => Some(env.INT)
-        case "INT.add" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x + y))
-        case "INT.sub" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x - y))
-        case "INT.ediv" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x / y))
-        case "INT.tmod" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x % y))
-        case "INT.abs" => Some(PrimitiveFunction1(s.symbol.str, env.INT, env.INT, (x: Int) => math.abs(x)))
-        case "INT.shr" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x >> y))
-        case "INT.not" => Some(PrimitiveFunction1(s.symbol.str, env.INT, env.INT, (x: Int) => ~x))
-        case "INT.xor" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.INT, (x: Int, y: Int) => x ^ y))
-        case "INT.ne" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x != y))
-        case "INT.gt" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x > y))
-        case "INT.ge" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x >= y))
-        case "INT.lt" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x < y))
-        case "INT.le" => Some(PrimitiveFunction2(s.symbol.str, env.INT, env.BOOLEAN, (x: Int, y: Int) => x <= y))
-        case "BOOL.or" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x || y))
-        case "BOOL.and" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x && y))
-        case "BOOL.xor" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x ^ y))
-        case "BOOL.ne" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x != y))
-        case "BOOL.not" => Some(PrimitiveFunction1(s.symbol.str, env.BOOLEAN, (x: Boolean) => !x))
-        case "BOOL.eq" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => x == y))
-        case "BOOL.implies" => Some(PrimitiveFunction2(s.symbol.str, env.BOOLEAN, env.BOOLEAN, (x: Boolean, y: Boolean) => !x || y))
-        //Todo: How to handle these?
-        case "BOOL.orElse" => Some(SimpleFreeLabel2(s.symbol.str))
-        case "BOOL.andThen" => Some(SimpleFreeLabel2(s.symbol.str))
-        case "KString" => Some(SimpleFreeLabel1(s.symbol.str))
-        case "#KRewrite" => Some(FunctionDefinedByRewritingLabel2(s.symbol.str))
-        case _ => None
-      }
+      case Some(kore.Value(v)) => env.uniqueLabels.get(v)
       case None => None
     }
   }
diff --git a/src/main/scala/org/kframework/kale/Environment.scala b/src/main/scala/org/kframework/kale/Environment.scala
index b18db38..cbd1883 100644
--- a/src/main/scala/org/kframework/kale/Environment.scala
+++ b/src/main/scala/org/kframework/kale/Environment.scala
@@ -7,6 +7,8 @@ import scala.collection._
 
 trait Environment extends KORELabels with Bottomize {
 
+  implicit protected val env: this.type = this
+
   trait HasEnvironment {
     val env = Environment.this
   }
@@ -31,7 +33,7 @@ trait Environment extends KORELabels with Bottomize {
   protected val unifier: MatcherOrUnifier
 
   def register(label: Label): Int = {
-    assert(!isSealed, "The environment is sealed")
+    assert(!isSealed, "Cannot register label " + label + " because the environment is sealed")
     assert(label != null)
 
     if (uniqueLabels.contains(label.name))
@@ -52,6 +54,15 @@ trait Environment extends KORELabels with Bottomize {
   override def toString = {
     "nextId: " + uniqueLabels.size + "\n" + uniqueLabels.mkString("\n")
   }
+
+  def SMTName(l: Label): String
+
+  def isZ3Builtin(l: Label): Boolean
+
+  implicit class WithSMTname(l: Label) {
+    def smtName: String = SMTName(l)
+  }
+
 }
 
 trait KORELabels {
diff --git a/src/main/scala/org/kframework/kale/builtin/BOOLEAN.scala b/src/main/scala/org/kframework/kale/builtin/BOOLEAN.scala
index 0395eb6..03845f5 100644
--- a/src/main/scala/org/kframework/kale/builtin/BOOLEAN.scala
+++ b/src/main/scala/org/kframework/kale/builtin/BOOLEAN.scala
@@ -1,12 +1,20 @@
 package org.kframework.kale.builtin
 
-import org.kframework.kale.Environment
+import org.kframework.kale.{DomainValue, Environment, Label, builtin}
 import org.kframework.kale.standard.ReferenceLabel
 
-trait HasBOOLEAN {
-  self: Environment =>
-
-  val BOOLEAN = new ReferenceLabel[Boolean]("Boolean")(this) {
+case class BOOLEAN()(implicit penv: Environment) extends Module("BOOLEAN") {
+  val Boolean = new ReferenceLabel[Boolean]("Boolean") {
     override protected[this] def internalInterpret(s: String): Boolean = s.toBoolean
   }
+
+  override val all: Set[Label] = Set(Boolean)
+}
+
+trait importBOOLEAN {
+  protected val env: Environment
+
+  val BOOLEAN = builtin.BOOLEAN()(env)
+
+  implicit def toBoolean(b: Boolean): DomainValue[Boolean] = BOOLEAN.Boolean(b)
 }
diff --git a/src/main/scala/org/kframework/kale/builtin/DOUBLE.scala b/src/main/scala/org/kframework/kale/builtin/DOUBLE.scala
index 550ab15..9893565 100644
--- a/src/main/scala/org/kframework/kale/builtin/DOUBLE.scala
+++ b/src/main/scala/org/kframework/kale/builtin/DOUBLE.scala
@@ -1,27 +1,28 @@
 package org.kframework.kale.builtin
 
 import org.kframework.kale.standard.ReferenceLabel
-import org.kframework.kale.{Environment, FunctionLabel2, Term}
+import org.kframework.kale.util.Named
+import org.kframework.kale.{FunctionLabel2, _}
 
-trait HasDOUBLE {
-  self: Environment =>
-
-  val DOUBLE = new ReferenceLabel[Double]("Double")(this) {
+case class DOUBLE()(implicit protected val penv: Environment) extends Module("DOUBLE") {
+  val Double = new ReferenceLabel[Double]("Double")(penv) {
     override protected[this] def internalInterpret(s: String): Double = s.toDouble
   }
-}
 
-trait HasDOUBLEdiv {
-  self: Environment with HasDOUBLE =>
-
-  val DOUBLEdiv = new HasEnvironment with FunctionLabel2 {
+  val div = new Named("_/Double_") with FunctionLabel2 {
     def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (_, DOUBLE(0)) => None
-      case (DOUBLE(0), b) if b.isGround => Some(DOUBLE(0))
-      case (DOUBLE(a), DOUBLE(b)) => Some(DOUBLE(a / b))
+      case (_, Double(0)) => None
+      case (Double(0), b) if b.isGround => Some(Double(0))
+      case (Double(a), Double(b)) => Some(Double(a / b))
       case _ => None
     }
-
-    override val name: String = "_/Double_"
   }
+
+  override lazy val all: Set[Label] = Set(Double)
+}
+
+trait importDOUBLE {
+  protected val env: Environment
+
+  val DOUBLE = builtin.DOUBLE()(env)
 }
diff --git a/src/main/scala/org/kframework/kale/builtin/ID.scala b/src/main/scala/org/kframework/kale/builtin/ID.scala
index fc2769c..00ccb78 100644
--- a/src/main/scala/org/kframework/kale/builtin/ID.scala
+++ b/src/main/scala/org/kframework/kale/builtin/ID.scala
@@ -1,14 +1,21 @@
 package org.kframework.kale.builtin
 
-import org.kframework.kale.{DomainValue, Environment}
+import org.kframework.kale.{DomainValue, Environment, Label}
 import org.kframework.kale.standard.ReferenceLabel
+import org.kframework.kale.builtin
 
-trait HasID {
-  self: Environment =>
-
-  val ID = new ReferenceLabel[Symbol]("ID")(this) {
+case class ID()(implicit protected val penv: Environment) extends Module("ID")   {
+  val Id = new ReferenceLabel[Symbol]("Id")(penv) {
     override protected[this] def internalInterpret(s: String): Symbol = Symbol(s)
   }
+  override val all: Set[Label] = Set(Id)
+}
+
+trait importID {
+  protected val env: Environment
+
+  val ID = builtin.ID()(env)
+
+  implicit def toID(s: Symbol): DomainValue[Symbol] = ID.Id(s)
 
-  implicit def toID(s: Symbol): DomainValue[Symbol] = ID(s)
 }
diff --git a/src/main/scala/org/kframework/kale/builtin/INT.scala b/src/main/scala/org/kframework/kale/builtin/INT.scala
index 891a354..8c98e14 100644
--- a/src/main/scala/org/kframework/kale/builtin/INT.scala
+++ b/src/main/scala/org/kframework/kale/builtin/INT.scala
@@ -1,111 +1,34 @@
 package org.kframework.kale.builtin
 
-import org.kframework.kale.standard.ReferenceLabel
-import org.kframework.kale.util.Named
 import org.kframework.kale._
+import org.kframework.kale.standard.ReferenceLabel
 
-trait HasINT {
-  self: Environment =>
-
-  val INT = new ReferenceLabel[Int]("Int")(this) {
-    override protected[this] def internalInterpret(s: String): Int = s.toInt
-  }
-
-  implicit def toINT(i: Int): DomainValue[Int] = INT(i)
-}
-
-trait HasINTbop extends HasINTplus with HasINTminus with HasINTmult with HasINTdiv with HasINTmod { self: Environment => }
-
-trait HasINTplus extends HasINT { self: Environment =>
-  val intPlus = new Named("_+Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(INT(a + b))
-      case _ => None
-    }
-    override def smtName: String = "+"
-  }
-}
-
-trait HasINTminus extends HasINT { self: Environment =>
-  val intMinus = new Named("_-Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(INT(a + b))
-      case _ => None
-    }
-    override def smtName: String = "-"
-  }
-}
-
-trait HasINTmult extends HasINT { self: Environment =>
-  val intMult = new Named("_*Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(INT(a * b))
-      case _ => None
-    }
-    override def smtName: String = "*"
-  }
-}
+case class INT(implicit protected val penv: Environment with importBOOLEAN) extends Module("INT") {
 
-trait HasINTdiv extends HasINT { self: Environment =>
-  val intDiv = new Named("_/Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-    //case (_, INT(0)) => None
-    //case (INT(0), b) if b.isGround => Some(INT(0))
-      case (INT(a), INT(b)) => Some(INT(a / b))
-      case _ => None
-    }
-    override def smtName: String = "div" // integer division, while "/" is real division.
-  }
-}
+  import penv._
 
-trait HasINTmod extends HasINT { self: Environment =>
-  val intMod = new Named("_%Int_")(self) with FunctionLabel2 {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(INT(a % b))
-      case _ => None
-    }
-    override def smtName: String = "mod" // z3 also has "rem", remainder.
+  val Int = new ReferenceLabel[Int]("Int") {
+    override protected[this] def internalInterpret(s: String): Int = s.toInt
   }
-}
 
-trait HasINTcmp extends HasINTlt with HasINTle with HasINTgt with HasINTge { self: Environment => }
+  val plus = PrimitiveFunction2[Int]("_+Int_", Int, _ + _)
+  val minus = PrimitiveFunction2[Int]("_-Int_", Int, _ - _)
+  val mult = PrimitiveFunction2[Int]("_*Int_", Int, _ * _)
+  val div = PrimitiveFunction2[Int]("_/Int_", Int, _ / _)
+  val mod = PrimitiveFunction2[Int]("_%Int_", Int, _ / _)
+  val lt = PrimitiveFunction2[Int, Boolean]("_<Int_", Int, BOOLEAN.Boolean, _ < _)
+  val le = PrimitiveFunction2[Int, Boolean]("_<=Int_", Int, BOOLEAN.Boolean, _ <= _)
+  val gt = PrimitiveFunction2[Int, Boolean]("_>Int_", Int, BOOLEAN.Boolean, _ > _)
+  val ge = PrimitiveFunction2[Int, Boolean]("_>=Int_", Int, BOOLEAN.Boolean, _ >= _)
 
-trait HasINTlt extends HasINT with HasBOOLEAN { self: Environment =>
-  val intLt = new Named("_<Int_")(self) with FunctionLabel2 with Z3Builtin {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(BOOLEAN(a < b))
-      case _ => None
-    }
-    override def smtName: String = "<"
-  }
+  lazy val all = Set(Int, plus, minus, mult, div, mod, lt, le, gt, ge)
 }
 
-trait HasINTle extends HasINT with HasBOOLEAN { self: Environment =>
-  val intLe = new Named("_<=Int_")(self) with FunctionLabel2 with Z3Builtin {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(BOOLEAN(a <= b))
-      case _ => None
-    }
-    override def smtName: String = "<="
-  }
-}
+trait importINT {
+  protected val env: Environment with importBOOLEAN
+  val BOOLEAN: builtin.BOOLEAN
 
-trait HasINTgt extends HasINT with HasBOOLEAN { self: Environment =>
-  val intGt = new Named("_>Int_")(self) with FunctionLabel2 with Z3Builtin {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(BOOLEAN(a > b))
-      case _ => None
-    }
-    override def smtName: String = ">"
-  }
-}
+  val INT = builtin.INT()(env)
 
-trait HasINTge extends HasINT with HasBOOLEAN { self: Environment =>
-  val intGe = new Named("_>=Int_")(self) with FunctionLabel2 with Z3Builtin {
-    def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match {
-      case (INT(a), INT(b)) => Some(BOOLEAN(a >= b))
-      case _ => None
-    }
-    override def smtName: String = ">="
-  }
+  implicit def toINT(i: Int): DomainValue[Int] = INT.Int(i)
 }
diff --git a/src/main/scala/org/kframework/kale/builtin/Module.scala b/src/main/scala/org/kframework/kale/builtin/Module.scala
new file mode 100644
index 0000000..597f285
--- /dev/null
+++ b/src/main/scala/org/kframework/kale/builtin/Module.scala
@@ -0,0 +1,16 @@
+package org.kframework.kale.builtin
+
+import org.kframework.kale.{Environment, Label, util}
+
+abstract class Module(val moduleName: String)(implicit val env: Environment) {
+
+  private def fullname(localName: String): String = localName + "@" + moduleName
+
+  protected abstract class LocalName[E <: Environment](val localName: String) extends util.Named(fullname(localName))
+
+  val all: Set[Label]
+
+  private lazy val labelName2Label = all.map(l => (l.name, l)).toMap
+
+  def apply(localName: String): Label = labelName2Label(fullname(localName))
+}
diff --git a/src/main/scala/org/kframework/kale/builtin/SET.scala b/src/main/scala/org/kframework/kale/builtin/SET.scala
index ccf3fdd..1b1fb28 100644
--- a/src/main/scala/org/kframework/kale/builtin/SET.scala
+++ b/src/main/scala/org/kframework/kale/builtin/SET.scala
@@ -4,7 +4,7 @@ import org.kframework.kale._
 
 import scala.collection.{Iterable, Set}
 
-case class SetLabel(name: String, identity: Term)(implicit val env: Environment with HasBOOLEAN) extends AssocWithIdLabel {
+case class SetLabel(name: String, identity: Term)(implicit val env: Environment with importBOOLEAN) extends AssocWithIdLabel {
   override def construct(l: Iterable[Term]): Term = SET(this, l.toSet)
 
   trait HasEnvironment {
@@ -23,7 +23,7 @@ case class SetLabel(name: String, identity: Term)(implicit val env: Environment
     val name = SetLabel.this.name + ".in"
   } with HasEnvironment with FunctionLabel2 {
     def f(s: Term, key: Term) = s match {
-      case set(elements) => Some(env.BOOLEAN(elements.contains(key)))
+      case set(elements) => Some(env.BOOLEAN.Boolean(elements.contains(key)))
     }
   }
 
diff --git a/src/main/scala/org/kframework/kale/builtin/STRING.scala b/src/main/scala/org/kframework/kale/builtin/STRING.scala
index efa6b5c..ad82236 100644
--- a/src/main/scala/org/kframework/kale/builtin/STRING.scala
+++ b/src/main/scala/org/kframework/kale/builtin/STRING.scala
@@ -1,14 +1,21 @@
 package org.kframework.kale.builtin
 
-import org.kframework.kale.{DomainValue, Environment}
+import org.kframework.kale.{DomainValue, Environment, Label}
 import org.kframework.kale.standard.ReferenceLabel
+import org.kframework.kale.builtin
 
-trait HasSTRING {
-  self: Environment =>
-
-  val STRING = new ReferenceLabel[String]("String")(this) {
+case class STRING()(implicit protected val penv: Environment) extends Module("STRING")   {
+  val String = new ReferenceLabel[String]("String")(penv) {
     override protected[this] def internalInterpret(s: String): String = s
   }
+  override val all: Set[Label] = Set(String)
+}
+
+trait importSTRING {
+  protected val env: Environment
+
+  val STRING = builtin.STRING()(env)
+
+  implicit def toSTRING(s: String): DomainValue[String] = STRING.String(s)
 
-  implicit def toSTRING(s: String): DomainValue[String] = STRING(s)
 }
diff --git a/src/main/scala/org/kframework/kale/km/KMEnvironment.scala b/src/main/scala/org/kframework/kale/km/KMEnvironment.scala
index 9d32af1..5d09f24 100644
--- a/src/main/scala/org/kframework/kale/km/KMEnvironment.scala
+++ b/src/main/scala/org/kframework/kale/km/KMEnvironment.scala
@@ -7,25 +7,38 @@ import org.kframework.kale._
 
 import scala.collection._
 
-trait HasBuiltin
-  extends HasINT with HasINTbop with HasINTcmp
-  with HasID
-  with HasBOOLEAN
-  with HasSTRING
-{ self: Environment => }
+trait importBuiltin
+  extends Environment with importBOOLEAN
+    with importINT // with HasINTbop with HasINTcmp
+    with importID
+    with importSTRING {
+
+  def SMTName(l: Label): String = l match {
+    case INT.mod => "mod"
+    case INT.lt => "<"
+    case INT.gt => ">"
+    case INT.le => "<="
+    case INT.ge => ">="
+  }
+
+  def isZ3Builtin(l: Label): Boolean = l match {
+    case _: Z3Builtin => true
+    case l => INT.all.contains(l)
+  }
 
-class KMEnvironment extends DNFEnvironment with HasBuiltin {
-  private implicit val env = this
+}
+
+class KMEnvironment extends DNFEnvironment with importBuiltin {
 
   private val sorts = mutable.Map[Label, Signature]()
 
   case class Signature(args: Seq[kale.Sort], target: kale.Sort)
 
-  def sortArgs(l: Label): Seq[kale.Sort] = sorts.get(l).map({ signature => signature.args}).getOrElse({
+  def sortArgs(l: Label): Seq[kale.Sort] = sorts.get(l).map({ signature => signature.args }).getOrElse({
     throw new AssertionError("Could not find Signature for label: " + l)
   })
 
-  def sortTarget(l: Label): kale.Sort = sorts.get(l).map({ signature => signature.target}).getOrElse({
+  def sortTarget(l: Label): kale.Sort = sorts.get(l).map({ signature => signature.target }).getOrElse({
     throw new AssertionError("Could not find Signature for label: " + l)
   })
 
@@ -54,4 +67,5 @@ class KMEnvironment extends DNFEnvironment with HasBuiltin {
   override lazy val substitutionMaker: (Substitution) => SubstitutionApply = new SubstitutionApply(_)
 
   override protected lazy val unifier = new MultiSortedUnifier(this)
+
 }
diff --git a/src/main/scala/org/kframework/kale/pretty/HasPretty.scala b/src/main/scala/org/kframework/kale/pretty/importPretty.scala
similarity index 74%
rename from src/main/scala/org/kframework/kale/pretty/HasPretty.scala
rename to src/main/scala/org/kframework/kale/pretty/importPretty.scala
index 5ea0d81..1f8f8d3 100644
--- a/src/main/scala/org/kframework/kale/pretty/HasPretty.scala
+++ b/src/main/scala/org/kframework/kale/pretty/importPretty.scala
@@ -1,17 +1,17 @@
 package org.kframework.kale.pretty
 
-import org.kframework.kale.builtin.HasSTRING
+import org.kframework.kale.builtin.importSTRING
 import org.kframework.kale.util.Named
 import org.kframework.kale._
 
-class PrettyWrapperLabel(implicit envv: Environment with HasPretty) extends Named("œ") with Label3 {
+class PrettyWrapperLabel(implicit envv: Environment with importPretty) extends Named("œ") with Label3 {
 
   import env._
 
   override def apply(_1: Term, _2: Term, _3: Term): Term = {
-    assert(_1.label == STRING)
+    assert(_1.label == STRING.String)
     assert(_2.label != this)
-    assert(_3.label == STRING)
+    assert(_3.label == STRING.String)
     PrettyWrapperHolder(this, _1, _2, _3)
   }
 
@@ -37,7 +37,7 @@ case class PrettyWrapperHolder(label: PrettyWrapperLabel, prefix: Term, content:
   override def _3: Term = suffix
 }
 
-trait HasPretty extends HasSTRING {
+trait importPretty extends importSTRING {
   self: Environment =>
 
   val PrettyWrapper = new PrettyWrapperLabel()(this)
@@ -45,7 +45,7 @@ trait HasPretty extends HasSTRING {
   def pretty(t: Term): String
 
   implicit class PrettyTerm(t: Term) {
-    def pretty: String = HasPretty.this.pretty(t)
+    def pretty: String = importPretty.this.pretty(t)
   }
 
 }
diff --git a/src/main/scala/org/kframework/kale/standard/DNFEnvironment.scala b/src/main/scala/org/kframework/kale/standard/DNFEnvironment.scala
index 49140fe..b66e9a2 100644
--- a/src/main/scala/org/kframework/kale/standard/DNFEnvironment.scala
+++ b/src/main/scala/org/kframework/kale/standard/DNFEnvironment.scala
@@ -4,8 +4,6 @@ import org.kframework.kale._
 import org.kframework.kale.util.Util
 
 trait DNFEnvironment extends Environment {
-  private implicit val env = this
-
   override val Truth: TruthLabel = standard.StandardTruthLabel()
 
   override val Top: Top = standard.TopInstance()
diff --git a/src/main/scala/org/kframework/kale/standard/StandardEnvironment.scala b/src/main/scala/org/kframework/kale/standard/StandardEnvironment.scala
index 8e54baf..081d730 100644
--- a/src/main/scala/org/kframework/kale/standard/StandardEnvironment.scala
+++ b/src/main/scala/org/kframework/kale/standard/StandardEnvironment.scala
@@ -3,16 +3,14 @@ package org.kframework.kale.standard
 import org.kframework.kale
 import org.kframework.kale.builtin._
 import org.kframework.kale.context.anywhere.AnywhereContextApplicationLabel
-import org.kframework.kale.pretty.{HasPretty, PrettyWrapperHolder}
+import org.kframework.kale.pretty.{importPretty, PrettyWrapperHolder}
 import org.kframework.kale.{standard, _}
 
 object StandardEnvironment {
   def apply(): StandardEnvironment = new StandardEnvironment {}
 }
 
-trait StandardEnvironment extends DNFEnvironment with HasBOOLEAN with HasINT with HasINTdiv with HasDOUBLE with HasSTRING with HasID with HasPretty {
-  private implicit val env = this
-
+trait StandardEnvironment extends DNFEnvironment with importBOOLEAN with importINT with importDOUBLE with importSTRING with importID with importPretty {
   val Hole = Variable("☐", Sort.K)
 
   val IfThenElse = new IfThenElseLabel()
@@ -31,7 +29,7 @@ trait StandardEnvironment extends DNFEnvironment with HasBOOLEAN with HasINT wit
     case l: NodeLabel => Seq.fill(l.arity)(Sort.K)
   }
 
-  override val substitutionMaker: (Substitution) => SubstitutionApply = new SubstitutionWithContext(_)
+  override val substitutionMaker: (Substitution) => SubstitutionApply = new SubstitutionWithContext(_)(this)
 
   protected override lazy val unifier = SingleSortedMatcher()(this)
 
@@ -39,4 +37,8 @@ trait StandardEnvironment extends DNFEnvironment with HasBOOLEAN with HasINT wit
     case PrettyWrapper(p, c, s) => p + pretty(c) + s
     case _ => t.toString
   }
+
+  override def SMTName(l: Label): String = ???
+
+  override def isZ3Builtin(l: Label): Boolean = ???
 }
diff --git a/src/main/scala/org/kframework/kale/term.scala b/src/main/scala/org/kframework/kale/term.scala
index b3b68d5..e579794 100644
--- a/src/main/scala/org/kframework/kale/term.scala
+++ b/src/main/scala/org/kframework/kale/term.scala
@@ -11,8 +11,6 @@ trait Label extends MemoizedHashCode with kore.Symbol {
 
   val name: String
 
-  def smtName: String = name
-
   val id: Int = env.register(this)
 
   override def equals(other: Any): Boolean = other match {
diff --git a/src/main/scala/org/kframework/kale/util/Implicits.scala b/src/main/scala/org/kframework/kale/util/Implicits.scala
index 6fa37b5..b02cabe 100644
--- a/src/main/scala/org/kframework/kale/util/Implicits.scala
+++ b/src/main/scala/org/kframework/kale/util/Implicits.scala
@@ -1,7 +1,7 @@
 package org.kframework.kale.util
 
 import org.kframework.kale._
-import org.kframework.kale.builtin.HasINT
+import org.kframework.kale.builtin.importINT
 import org.kframework.kale.standard.{SimpleFreeLabel2, StandardEnvironment}
 
 import scala.language.implicitConversions
diff --git a/src/main/scala/org/kframework/kale/z3.scala b/src/main/scala/org/kframework/kale/z3.scala
index 8484c49..c947f1e 100644
--- a/src/main/scala/org/kframework/kale/z3.scala
+++ b/src/main/scala/org/kframework/kale/z3.scala
@@ -50,7 +50,7 @@ class z3(val env: Environment, val symbolsSeq: Seq[Seq[Label]]) {
     def getFunctionSymbols(term: Term): Set[Any] = term match {
       case t:Node =>
         val decls = t.children.flatMap(getFunctionSymbols).toSet
-        if (!t.label.isInstanceOf[Z3Builtin]) decls + t.label
+        if (!env.isZ3Builtin(t.label)) decls + t.label
         else decls
       case _:Variable => Set(term)
       case _:DomainValue[_] => Set()
@@ -64,7 +64,6 @@ class z3(val env: Environment, val symbolsSeq: Seq[Seq[Label]]) {
       case v:Variable => "(declare-const " + v.name + " " + v.sort.smtName + ")\n"
       case l:FreeLabel0 => "(declare-const " + l.smtName + " " + sortTarget(l).smtName + ")\n"
       case l:FreeLabel => "(declare-fun " + l.smtName + " (" + sortArgs(l).map(_.smtName).mkString(" ") + ") " + sortTarget(l).smtName + ")\n"
-      case _ => ???
     }).mkString
     // remaining sorts not defined by constructor datatypes
     val sorts: Set[Sort] = symbols.flatMap({
diff --git a/src/test/scala/org/kframework/kale/IMPCommonSignature.scala b/src/test/scala/org/kframework/kale/IMPCommonSignature.scala
index 024de1f..0ce69f3 100644
--- a/src/test/scala/org/kframework/kale/IMPCommonSignature.scala
+++ b/src/test/scala/org/kframework/kale/IMPCommonSignature.scala
@@ -1,9 +1,9 @@
 package org.kframework.kale
 
-import org.kframework.kale.builtin.{HasINT, HasINTdiv, MapLabel}
+import org.kframework.kale.builtin.{importINT, MapLabel}
 import org.kframework.kale.standard._
 
-class IMPCommonSignature(implicit val env: Environment with HasINT with HasINTdiv) {
+class IMPCommonSignature(implicit val env: Environment with importINT) {
   import env._
 
   def lhs(t: Term): Term = t match {
diff --git a/src/test/scala/org/kframework/kale/ImpOnSkalaTest.scala b/src/test/scala/org/kframework/kale/ImpOnSkalaTest.scala
index bef50e8..a15a282 100644
--- a/src/test/scala/org/kframework/kale/ImpOnSkalaTest.scala
+++ b/src/test/scala/org/kframework/kale/ImpOnSkalaTest.scala
@@ -14,7 +14,7 @@ import org.kframework.kore.extended.implicits._
 
 class ImpOnSkalaTest extends FreeSpec {
 
-  "IMP" in {
+  "IMP" ignore {
     val defaultBuilders: Builders = DefaultBuilders
     val koreParser = parser.TextToKore(defaultBuilders)
     val imp = Source.fromResource("imp.kore")
diff --git a/src/test/scala/org/kframework/kale/ImpSpec.scala b/src/test/scala/org/kframework/kale/ImpSpec.scala
index 107b5f4..5c8102e 100644
--- a/src/test/scala/org/kframework/kale/ImpSpec.scala
+++ b/src/test/scala/org/kframework/kale/ImpSpec.scala
@@ -85,7 +85,6 @@ object IMP {
   import signature._
 
   import env._
-  import builtin._
 
   val ints = new standard.AssocWithIdListLabel("_,_", emptyIntList())
   val kseq = new standard.AssocWithIdListLabel("_~>_", emptyk())
@@ -96,7 +95,7 @@ object IMP {
     def f(_1: Term): Option[Term] = Some(Truth(_1.label == label))
   }
 
-  val isInt = isSort(INT)
+  val isInt = isSort(INT.Int)
 
   //  // AExp
   //  rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
@@ -135,7 +134,7 @@ object IMP {
 
   val rules = Set(
     T(k(kseq(Rewrite(X, I), R)), state(statesMap(varBinding(X, I), SO))),
-    T(k(kseq(Rewrite(div(And(I1, isInt(I1)), And(I2, isInt(I2))), intDiv(I1, I2)), R)), S)
+    T(k(kseq(Rewrite(div(And(I1, isInt(I1)), And(I2, isInt(I2))), INT.div(I1, I2)), R)), S)
   ) map (t => Rewrite(lhs(t), rhs(t)))
 
   env.seal()
diff --git a/src/test/scala/org/kframework/kale/KaleSpec.scala b/src/test/scala/org/kframework/kale/KaleSpec.scala
index dbcf5a9..39b3196 100644
--- a/src/test/scala/org/kframework/kale/KaleSpec.scala
+++ b/src/test/scala/org/kframework/kale/KaleSpec.scala
@@ -31,11 +31,11 @@ class KaleSpec extends FreeSpec {
     val y: DomainValue[Int] = 3
 
     "Int" in {
-      assert(x == INT(2))
+      assert(x == INT.Int(2))
       assert(x != y)
 
       assert(x.data == 2)
-      assert(x.label == INT)
+      assert(x.label == INT.Int)
     }
     //    "+" in {
     //      assert(x + y == INT(5))
diff --git a/src/test/scala/org/kframework/kale/Play.sc b/src/test/scala/org/kframework/kale/Play.sc
new file mode 100644
index 0000000..94960c2
--- /dev/null
+++ b/src/test/scala/org/kframework/kale/Play.sc
@@ -0,0 +1,20 @@
+
+import language.dynamics
+
+trait Foo extends Dynamic {
+  def applyDynamic(m: String)(args: Any*) = {
+    "dynamic"
+  }
+}
+
+trait Bar extends Foo {
+  def a(): String = {
+    "a"
+  }
+}
+
+val x: Foo = new Bar {}
+
+x.a()
+
+x.b()
\ No newline at end of file
diff --git a/src/test/scala/org/kframework/kale/Play.scala b/src/test/scala/org/kframework/kale/Play.scala
deleted file mode 100644
index a9fbb3d..0000000
--- a/src/test/scala/org/kframework/kale/Play.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-package org.kframework.kale
-
-import org.kframework.kale._
-import org.kframework.kale.standard._
-
diff --git a/src/test/scala/org/kframework/kale/km/IMPSpec.scala b/src/test/scala/org/kframework/kale/km/IMPSpec.scala
index 8daf92d..af7d29e 100644
--- a/src/test/scala/org/kframework/kale/km/IMPSpec.scala
+++ b/src/test/scala/org/kframework/kale/km/IMPSpec.scala
@@ -29,8 +29,8 @@ class IMPSpec extends FreeSpec {
   import ImpSorts._
 
   // sortify builtin symbols
-  sorted(ID, Id)
-  sorted(INT, Int)
+  sorted(ID.Id, Id)
+  sorted(INT.Int, Int)
 
   // import/sortify common symbols
   val signature = new IMPCommonSignature()
@@ -78,7 +78,7 @@ class IMPSpec extends FreeSpec {
   // semantics
   val rules = Set(
     T(k(kseq(Rewrite(X, I), R)), state(statesMap(varBinding(X, I), SO))),
-    T(k(kseq(Rewrite(div(I1, I2), intDiv(I1, I2)), R)), S)
+    T(k(kseq(Rewrite(div(I1, I2), INT.div(I1, I2)), R)), S)
   ) map (t => Rewrite(lhs(t), rhs(t)))
 
   env.seal()
@@ -89,7 +89,7 @@ class IMPSpec extends FreeSpec {
   "first test" in {
     assert(unify(X, 'foo) === Equality(X, 'foo))
     assert(unify(X, Y) === Equality(X, Y))
-    assert(unify(X, INT(2)) === Bottom)
+    assert(unify(X, INT.Int(2)) === Bottom)
 
     assert(unify(plus(E1,E2), leq(E1,E2)) == Bottom)
 
diff --git a/src/test/scala/org/kframework/kale/km/RewriteTest.scala b/src/test/scala/org/kframework/kale/km/RewriteTest.scala
index 2f731c6..ff93722 100644
--- a/src/test/scala/org/kframework/kale/km/RewriteTest.scala
+++ b/src/test/scala/org/kframework/kale/km/RewriteTest.scala
@@ -18,8 +18,8 @@ class RewriteTest extends FreeSpec {
   import Sorts._
 
   // sortify builtin symbols
-  sorted(ID, Id)
-  sorted(INT, Int)
+  sorted(ID.Id, Id)
+  sorted(INT.Int, Int)
 
   // symbol declarations
   val a = SimpleFreeLabel0("a"); sorted(a, K)
@@ -71,15 +71,15 @@ class RewriteTest extends FreeSpec {
     val Z = Variable("Z", Int)
 
     val r1 = Rewrite(
-      And(Seq(p(X), Equality(intGt(X,INT(0)), BOOLEAN(true)))), // p(x) /\ x > 0
+      And(Seq(p(X), Equality(INT.gt(X,INT.Int(0)), BOOLEAN.Boolean(true)))), // p(x) /\ x > 0
       q(X)
     )
     val r2 = Rewrite(
-      And(Seq(q(X), Equality(intGe(X,INT(0)), BOOLEAN(true)))), // q(x) /\ x >= 0
+      And(Seq(q(X), Equality(INT.ge(X,INT.Int(0)), BOOLEAN.Boolean(true)))), // q(x) /\ x >= 0
       c()
     )
     val r3 = Rewrite(
-      And(Seq(q(X), Equality(intLt(X,INT(0)), BOOLEAN(true)))), // q(x) /\ x < 0
+      And(Seq(q(X), Equality(INT.lt(X,INT.Int(0)), BOOLEAN.Boolean(true)))), // q(x) /\ x < 0
       d()
     )
 
@@ -90,7 +90,7 @@ class RewriteTest extends FreeSpec {
     assert(
       rewriter(Set(r1)).searchStep(t1)
         ==
-      And(Seq(q(X), Equality(intGt(X,INT(0)), BOOLEAN(true))))
+      And(Seq(q(X), Equality(INT.gt(X,INT.Int(0)), BOOLEAN.Boolean(true))))
     )
 
     // rule p(x:Int) => q(x) if x > 0
@@ -101,7 +101,7 @@ class RewriteTest extends FreeSpec {
     assert(
       rr.searchStep(rr.searchStep(t1))
         ==
-      And(Seq(c(), Equality(intGe(X,INT(0)), BOOLEAN(true)), Equality(intGt(X,INT(0)), BOOLEAN(true))))
+      And(Seq(c(), Equality(INT.ge(X,INT.Int(0)), BOOLEAN.Boolean(true)), Equality(INT.gt(X,INT.Int(0)), BOOLEAN.Boolean(true))))
     )
 
   }
diff --git a/src/test/scala/org/kframework/kale/tests/FooTest.scala b/src/test/scala/org/kframework/kale/tests/FooTest.scala
new file mode 100644
index 0000000..2cca9b7
--- /dev/null
+++ b/src/test/scala/org/kframework/kale/tests/FooTest.scala
@@ -0,0 +1,28 @@
+package org.kframework.kale.tests
+
+import org.kframework.kale._
+import org.kframework.kale.builtin.{importINT}
+import org.kframework.kale.standard.DNFEnvironment
+import org.scalatest.FreeSpec
+
+class FooTest extends FreeSpec{
+  "foo" in {
+    implicit val env = new DNFEnvironment() {
+      override lazy val substitutionMaker: (Substitution) => SubstitutionApply = ???
+      override protected lazy val unifier: MatcherOrUnifier = ???
+
+      override def sort(l: Label, children: Seq[Term]): Sort = ???
+
+      override def sortArgs(l: Label): Seq[Sort] = ???
+
+      override def sortTarget(l: Label): Sort = ???
+
+      override def SMTName(l: Label): String = ???
+
+      override def isZ3Builtin(l: Label): Boolean = ???
+    }
+
+    println(env.isInstanceOf[importINT])
+
+  }
+}
diff --git a/src/test/scala/org/kframework/kale/tests/TestSetup.scala b/src/test/scala/org/kframework/kale/tests/TestSetup.scala
index 7cdd33f..0fa602d 100644
--- a/src/test/scala/org/kframework/kale/tests/TestSetup.scala
+++ b/src/test/scala/org/kframework/kale/tests/TestSetup.scala
@@ -30,7 +30,7 @@ trait TestSetup {
   val foo = SimpleFreeLabel2("foo")
   val bar = SimpleFreeLabel1("bar")
   val buz = SimpleFreeLabel2("buz")
-  val (a, b, c, d, e) = (STRING("a"), STRING("b"), STRING("c"), STRING("d"), STRING("e"))
+  val (a, b, c, d, e) = (STRING.String("a"), STRING.String("b"), STRING.String("c"), STRING.String("d"), STRING.String("e"))
   val matched = SimpleFreeLabel1("matched")
   val traversed = SimpleFreeLabel1("traversed")
   val andMatchingY = SimpleFreeLabel0("andMatchingY")
diff --git a/src/test/scala/org/kframework/kale/util/CodecTest.scala b/src/test/scala/org/kframework/kale/util/CodecTest.scala
index ff40c46..01d7ac8 100644
--- a/src/test/scala/org/kframework/kale/util/CodecTest.scala
+++ b/src/test/scala/org/kframework/kale/util/CodecTest.scala
@@ -17,7 +17,7 @@ class CodecTest extends FreeSpec {
 
   import env._
 
-  val pattern = foo(3, STRING("bar"))
+  val pattern = foo(3, STRING.String("bar"))
 
   object TestAtt extends Att[Int] {
     override def toString = "test"
@@ -39,13 +39,13 @@ class CodecTest extends FreeSpec {
 
   "decode int" in {
     val actual = decode[Term]("{\"label\":\"Int\",\"att\":{},\"data\":\"3\"}")
-    val expected = Right(INT(3))
+    val expected = Right(INT.Int(3))
     assert(actual === expected)
   }
 
   "decode string" in {
     val actual = decode[Term]("{\"label\":\"String\",\"att\":{},\"data\":\"bar\"}")
-    val expected = Right(STRING("bar"))
+    val expected = Right(STRING.String("bar"))
     assert(actual === expected)
   }
 
@@ -65,7 +65,7 @@ class CodecTest extends FreeSpec {
   }
 
   "att encoding" in {
-    val expectedTerm: Term = INT(3)
+    val expectedTerm: Term = INT.Int(3)
     expectedTerm.att(TestAtt)
 
     val expectedJson = "{\"label\":\"Int\",\"att\":{\"test\":0},\"data\":\"3\"}"