diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index e444d225de8427ebbce9890d030274a2879a96ec..ea488c76ea721e536c02fb7bf512eac63ca1669f 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -166,7 +166,7 @@ trait ASTExtractors {
        * objects of case classes (or any synthetic class). */
       def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
         case ClassDef(_, name, tparams, impl) if ((cd.symbol.isModuleClass || cd.symbol.hasPackageFlag) && tparams.isEmpty && !cd.symbol.isSynthetic) => {
-          Some((name.toString, impl))
+          Some((if (name.toString == "package") cd.symbol.owner.name.toString else name.toString, impl))
         }
         case _ => None
       }
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 51338cb30628baaee0f5b9f03873deb818fd3b22..e34b95c9b2adff3d93c54e75e082c4f5d48768ec 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -229,6 +229,7 @@ trait CodeExtraction extends ASTExtractors {
 
         // Phase 6, we create modules and extract bodies
         templates.map{ case (name, templ) => extractObjectDef(name, templ) }
+
       } catch {
         case icee: ImpureCodeEncounteredException =>
           icee.emit()
@@ -1264,6 +1265,9 @@ trait CodeExtraction extends ASTExtractors {
             case (IsTyped(a1, mt: MapType), "updated", List(k, v)) =>
               MapUnion(a1, FiniteMap(Seq((k, v))).setType(mt)).setType(mt)
 
+            case (IsTyped(a1, mt1: MapType), "++", List(IsTyped(a2, mt2: MapType)))  if mt1 == mt2 =>
+              MapUnion(a1, a2).setType(mt1)
+              
             case (_, name, _) =>
               outOfSubsetError(tr, "Unknown call to "+name)
           }
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 06658e31d33f298d042a7d37ccddcc2a71311697..6200332b87cf6388e1c2d0edcf062e4f983c02af 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -60,7 +60,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
       run.compile(command.files)
 
 
-      val pgm = Program(FreshIdentifier("<program>"), compiler.leonExtraction.modules)
+      val pgm = Program(FreshIdentifier("__program"), compiler.leonExtraction.modules)
       ctx.reporter.debug(pgm.asString(ctx))
       pgm
     } else {