diff --git a/library/lang/synthesis/Oracle.scala b/library/lang/synthesis/Oracle.scala
index 34867e3f9ebabfae32d6e9fd7d6238345247ed36..ac345d9900e883d4f4d60c7d2891abd6bd488b42 100644
--- a/library/lang/synthesis/Oracle.scala
+++ b/library/lang/synthesis/Oracle.scala
@@ -8,6 +8,7 @@ import leon.lang._
 import scala.annotation._
 
 @implicitNotFound("No Oracle available for this source of non-determinism, please provide an implicit arg <: Oracle[T]")
+@ignore
 @library
 abstract class Oracle[T] {
   def head: T = this match {
@@ -26,5 +27,7 @@ abstract class Oracle[T] {
   }
 }
 
+@ignore
 case class Node[T](l: Oracle[T], v: T, r: Oracle[T]) extends Oracle[T];
+@ignore
 case class Leaf[T](v: T) extends Oracle[T];