diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index 25dd1288d421ecf49d0136948b5392abae64c51b..f329b589abb38457cd8f53e1ebe15209c311f201 100644
--- a/library/lazy/package.scala
+++ b/library/lazy/package.scala
@@ -22,10 +22,10 @@ object $ {
    * Should be used only in ensuring.
    * TODO: enforce this.
    */
-  @extern @library
+  @extern
   def inState[T] : Set[$[T]] = sys.error("inState method is not executable!")
 
-  @extern @library
+  @extern
   def outState[T] : Set[$[T]] = sys.error("outState method is not executable")
 
   /**
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 0e5aa269cf00234e08348064c512ebf35ac8a15c..a33ec69e587f35c183d93932cabe7b340e94d4d4 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -201,7 +201,7 @@ trait CodeGeneration {
       funDef.fullBody
     } else {
       funDef.body.getOrElse(
-        if(funDef.annotations contains "library") {
+        if(funDef.annotations contains "extern") {
           Error(funDef.id.getType, "Body of " + funDef.id.name + " not implemented at compile-time and still executed.")
         } else {
           throw CompilationException("Can't compile a FunDef without body: "+funDef.id.name)