diff --git a/library/util/Random.scala b/library/util/Random.scala
index 8a942e31be0d8ec4df6a9914bb83e5799982404f..e8efac0bd1688cd480ab3d7c97b18569025196df 100644
--- a/library/util/Random.scala
+++ b/library/util/Random.scala
@@ -8,21 +8,26 @@ import leon.lang.xlang._
 object Random {
 
   @library
+  @isabelle.noBody()
   def nextBoolean(): Boolean = epsilon((x: Boolean) => true)
 
   @library
+  @isabelle.noBody()
   def nextInt(): Int = epsilon((x: Int) => true)
 
   @library
+  @isabelle.noBody()
   def nextInt(max: Int): Int = {
     require(max > 0)
     epsilon((x: Int) => x >= 0 && x < max)
   } ensuring(res => res >= 0 && res < max)
 
   @library
+  @isabelle.noBody()
   def nextBigInt(): BigInt = epsilon((x: BigInt) => true)
 
   @library
+  @isabelle.noBody()
   def nextBigInt(max: BigInt): BigInt = {
     require(max > 0)
     epsilon((x: BigInt) => x >= 0 && x < max)