diff --git a/src/main/scala/leon/evaluators/ScalacEvaluator.scala b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
index 2b13d2655b43bd5e9a41fd236a8acb963d106356..2356bdf33329288907d8d48ccb6f9cdd07c8596a 100644
--- a/src/main/scala/leon/evaluators/ScalacEvaluator.scala
+++ b/src/main/scala/leon/evaluators/ScalacEvaluator.scala
@@ -163,9 +163,6 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
   }
 
   def leonToScalac(e: Expr): AnyRef = e match {
-    case eo: ExternalObject =>
-      eo
-
     case CharLiteral(v) =>
       new java.lang.Character(v)
 
@@ -274,7 +271,7 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
 
       FiniteMap(s.iterator.map {
         case (k, v) => scalacToLeon(k, ktpe) -> scalacToLeon(v, vtpe)
-      }.toSeq, ktpe, vtpe)
+      }.toMap, ktpe, vtpe)
 
     case FunctionType(_, _) =>
       unsupported("It is not possible to pass a closure from @extern back to leon")
@@ -459,8 +456,6 @@ class ScalacEvaluator(ev: Evaluator, ctx: LeonContext, pgm: Program) extends Leo
   }
 }
 
-case class ExternalObject(o: Any, getType: TypeTree) extends Expr with Terminal
-
 object LeonJVMCallBacks {
   def callBack(token: Int, className: String, methodName: String, args: Array[AnyRef]): AnyRef = {
     val ev = RuntimeResources.get[ScalacEvaluator](token)