diff --git a/library/leon/lang/StaticChecks.scala b/library/leon/lang/StaticChecks.scala
index e53f2def0bac9146a4a2ee615224e321b7b0ee6d..1b6e20569834f8683a0efd8bfb04d8c489d378b3 100644
--- a/library/leon/lang/StaticChecks.scala
+++ b/library/leon/lang/StaticChecks.scala
@@ -6,6 +6,7 @@ import scala.language.implicitConversions
 object StaticChecks {
 
   case class Ensuring[A](x: A) {
+    @library
     def ensuring(cond: (A) => Boolean): A = x
   }
 
diff --git a/library/leon/webDSL/webDescription/WebPage.scala b/library/leon/webDSL/webDescription/WebPage.scala
index c00b219d74f3dedaae1b3f0e13d30102b3ddd23c..274b75187222e8378efd0700014941416a3d0511 100644
--- a/library/leon/webDSL/webDescription/WebPage.scala
+++ b/library/leon/webDSL/webDescription/WebPage.scala
@@ -10,6 +10,7 @@ case class StyleRule(target: String, rules: List[WebStyle])
 
 @library
 case class StyleSheet(elems: List[StyleRule]) {
+  @library
   def apply(l: List[StyleRule]): StyleSheet = {
     StyleSheet(elems ++ l)
   }
@@ -23,7 +24,8 @@ case class StyleSheet(elems: List[StyleRule]) {
   }
 }
 
-object WebPage { 
+object WebPage {
+  @library
   def apply(main: WebElement): WebPage = {
     WebPage(main, StyleSheet(Nil()))
   }
diff --git a/library/leon/webDSL/webDescription/package.scala b/library/leon/webDSL/webDescription/package.scala
index 188ddece71034265038aa7d64ac4888c7d778534..ca052d39dea63af443a0e63b3e1640c0fe48ad5b 100644
--- a/library/leon/webDSL/webDescription/package.scala
+++ b/library/leon/webDSL/webDescription/package.scala
@@ -4,6 +4,7 @@ import leon.lang._
 import leon.annotation._
 
 package object webDescription {
+  @library
   val Style = StyleSheet(Nil())
   
   @library