diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index b51a0746b3d2665b659885fbf3332e2f499fa9c2..22fa23f61462334e238734c2bd50c7150502ed15 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -34,7 +34,6 @@ object Main {
       LeonFlagOptionDef ("termination", "--termination",        "Check program termination"),
       LeonFlagOptionDef ("synthesis",   "--synthesis",          "Partial synthesis of choose() constructs"),
       LeonFlagOptionDef ("xlang",       "--xlang",              "Support for extra program constructs (imperative,...)"),
-      LeonFlagOptionDef ("library",     "--library",            "Inject Leon standard library"),
       LeonValueOptionDef("solvers",     "--solvers=s1,s2",      "Use solvers s1 and s2 (fairz3,enum,smt)"),
       LeonValueOptionDef("debug",       "--debug=<sections..>", "Enables specific messages"),
       LeonFlagOptionDef ("noop",        "--noop",               "No operation performed, just output program"),
@@ -143,8 +142,6 @@ object Main {
         settings = settings.copy(termination = value)
       case LeonFlagOption("synthesis", value) =>
         settings = settings.copy(synthesis = value)
-      case LeonFlagOption("library", value) =>
-        settings = settings.copy(injectLibrary = value)
       case LeonFlagOption("xlang", value) =>
         settings = settings.copy(xlang = value)
       case LeonValueOption("solvers", ListValue(ss)) =>
@@ -231,19 +228,12 @@ object Main {
     pipeProcess
   }
 
-  def main(args : Array[String]) {
+  def main(args: Array[String]) {
     val argsl = args.toList
 
-    // By default we add --library from Main
-    val realArgs = if (!args.exists(_.contains("--library"))) {
-      "--library" :: argsl
-    } else {
-      argsl
-    }
-
     // Process options
     val ctx = try {
-      processOptions(realArgs)
+      processOptions(argsl)
     } catch {
       case LeonFatalError(None) =>
         sys.exit(1)
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 52ede3a613f3314b995696243b6dfb027103c60a..4ad409af285d8aaaebf72fd9d82254dcb8e94d93 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -11,6 +11,5 @@ case class Settings(
   val synthesis: Boolean               = false,
   val xlang: Boolean                   = false,
   val verify: Boolean                  = true,
-  val injectLibrary: Boolean           = false,
   val selectedSolvers: Set[String]     = Set("fairz3")
 )
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index 7ab53108831841b671e46a7b12c19ef80f748fa2..970c82ca02810ab180f6ddd985f7c0aa0a9d4ee1 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -35,15 +35,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
     settings.Yrangepos.value = true
     settings.skip.value      = List("patmat")
 
-    val libFiles = Build.libFiles
-    
-    val injected = if (ctx.settings.injectLibrary) {
-      libFiles
-    } else {
-      libFiles.filter(f => (f.contains("/lang/") && !f.contains("/lang/string/")) || f.contains("/annotation/"))
-    }
-
-    val compilerOpts = injected ::: args.filterNot(_.startsWith("--"))
+    val compilerOpts = Build.libFiles ::: args.filterNot(_.startsWith("--"))
 
     val command = new CompilerCommand(compilerOpts, settings) {
       override val cmdName = "leon"