diff --git a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
index 2850de3d2..7c084e830 100644
--- a/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
+++ b/core/src/main/scala/stainless/extraction/imperative/AntiAliasing.scala
@@ -261,7 +261,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
         // * `selectResult` selects the first element of the tuple returned by the transformed function
         // (the others elements are the "updated" version of the mutated parameters).
         // By default, it should be set to `true`.
-        // However, in the particular case of `unfold(fn(...))`, we would like *not* to have this selection be performed
+        // However, in the particular case of `unfolding(fn(...))`, we would like *not* to have this selection be performed
         // due to the following. `AntiAliasing` will transform this call to:
         //   unfold {
         //      val res = fn(...)
@@ -1055,7 +1055,7 @@ class AntiAliasing(override val s: Trees)(override val t: s.type)(using override
 
         object UnfoldOpaque {
           def unapply(e: Expr): Option[(Identifier, FunctionInvocation)] = e match {
-            case FunctionInvocation(id @ ast.SymbolIdentifier("stainless.lang.unfold"), Seq(_), Seq(fi: s.FunctionInvocation)) =>
+            case FunctionInvocation(id @ ast.SymbolIdentifier("stainless.lang.unfolding"), Seq(_), Seq(fi: s.FunctionInvocation)) =>
               Some((id, fi))
             case _ => None
           }
diff --git a/core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala b/core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala
index 249e6ff33..4a8192fc5 100644
--- a/core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala
+++ b/core/src/main/scala/stainless/extraction/inlining/UnfoldOpaque.scala
@@ -24,7 +24,7 @@ class UnfoldOpaque(override val s: Trees, override val t: Trees)
 
     override def transform(e: Expr, env: Env): t.Expr = {
       e match {
-        case s.FunctionInvocation(ast.SymbolIdentifier("stainless.lang.unfold"), Seq(_), Seq(maybeFi)) =>
+        case s.FunctionInvocation(ast.SymbolIdentifier("stainless.lang.unfolding"), Seq(_), Seq(maybeFi)) =>
           // Lookup the bindings recursively to unveil a call to a function which we would need to unfold
           val r = dealiasedAndStripped(maybeFi, env)
           r match {
diff --git a/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala b/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala
index 2e8b840f7..599dae69d 100644
--- a/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala
+++ b/frontends/benchmarks/imperative/invalid/OpaqueMutation1.scala
@@ -14,8 +14,8 @@ object OpaqueMutation1 {
       @ghost val oldBox = snapshot(this)
       cnt += 1
       ghostExpr {
-        unfold(secretSauce(other))
-        unfold(oldBox.secretSauce(other))
+        unfolding(secretSauce(other))
+        unfolding(oldBox.secretSauce(other))
         check(oldBox.secretSauce(other) + 1 == this.secretSauce(other))
       }
     }.ensuring(_ => old(this).secretSauce(other) + 1 == this.secretSauce(other))
@@ -29,4 +29,4 @@ object OpaqueMutation1 {
     // Therefore, the following is incorrect (but it holds for `b.other`, see the other `valid/OpaqueMutation`)
     assert(oldBox.secretSauce(oldBox.other) + 1 == b.secretSauce(oldBox.other))
   }
-}
\ No newline at end of file
+}
diff --git a/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala b/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala
index 6f0498bc7..69d8a083c 100644
--- a/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala
+++ b/frontends/benchmarks/imperative/invalid/OpaqueMutation2.scala
@@ -15,8 +15,8 @@ object OpaqueMutation2 {
       @ghost val oldBox = snapshot(this)
       cnt += 1
       ghostExpr {
-        unfold(secretSauce(smallerBox.otherCnt))
-        unfold(oldBox.secretSauce(smallerBox.otherCnt))
+        unfolding(secretSauce(smallerBox.otherCnt))
+        unfolding(oldBox.secretSauce(smallerBox.otherCnt))
         check(oldBox.secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt))
       }
     }.ensuring(_ => old(this).secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt))
@@ -30,4 +30,4 @@ object OpaqueMutation2 {
     // Therefore, the following is incorrect (but it holds for `b.other`, see the other `valid/OpaqueMutation`)
     assert(oldBox.secretSauce(oldBox.smallerBox.otherCnt) + 1 == b.secretSauce(oldBox.smallerBox.otherCnt))
   }
-}
\ No newline at end of file
+}
diff --git a/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala b/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala
index 577b7c5bf..e30cb23eb 100644
--- a/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala
+++ b/frontends/benchmarks/imperative/valid/OpaqueMutation1.scala
@@ -13,8 +13,8 @@ object OpaqueMutation1 {
       @ghost val oldBox = snapshot(this)
       cnt += 1
       ghostExpr {
-        unfold(secretSauce(other))
-        unfold(oldBox.secretSauce(other))
+        unfolding(secretSauce(other))
+        unfolding(oldBox.secretSauce(other))
         check(oldBox.secretSauce(other) + 1 == this.secretSauce(other))
       }
     }.ensuring(_ => old(this).secretSauce(other) + 1 == this.secretSauce(other))
@@ -24,8 +24,8 @@ object OpaqueMutation1 {
     def incrementPure(): (Unit, Box) = {
       val newThis = Box(cnt + 1, other)
       ghostExpr {
-        unfold(newThis.secretSauce(other))
-        unfold(this.secretSauce(other))
+        unfolding(newThis.secretSauce(other))
+        unfolding(this.secretSauce(other))
         check(this.secretSauce(other) + 1 == newThis.secretSauce(other))
       }
       ((), newThis)
@@ -67,4 +67,4 @@ object OpaqueMutation1 {
     assert(oldB2.secretSauce(newB2.other) + 1 == newB2.secretSauce(newB2.other))
     assert(cond ==> (oldB2.secretSauce(newB.other) + 1 == newB.secretSauce(newB.other)))
   }
-}
\ No newline at end of file
+}
diff --git a/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala b/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala
index 0e9e914f8..5a3037e35 100644
--- a/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala
+++ b/frontends/benchmarks/imperative/valid/OpaqueMutation2.scala
@@ -15,8 +15,8 @@ object OpaqueMutation2 {
       @ghost val oldBox = snapshot(this)
       cnt += 1
       ghostExpr {
-        unfold(secretSauce(smallerBox.otherCnt))
-        unfold(oldBox.secretSauce(smallerBox.otherCnt))
+        unfolding(secretSauce(smallerBox.otherCnt))
+        unfolding(oldBox.secretSauce(smallerBox.otherCnt))
         check(oldBox.secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt))
       }
     }.ensuring(_ => old(this).secretSauce(smallerBox.otherCnt) + 1 == this.secretSauce(smallerBox.otherCnt))
@@ -41,4 +41,4 @@ object OpaqueMutation2 {
     assert(oldB2.secretSauce(b2.smallerBox.otherCnt) + 1 == b2.secretSauce(b2.smallerBox.otherCnt))
     assert(cond ==> (oldB2.secretSauce(b.smallerBox.otherCnt) + 1 == b.secretSauce(b.smallerBox.otherCnt)))
   }
-}
\ No newline at end of file
+}
diff --git a/frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala b/frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala
index 47b02ce69..24e50a640 100644
--- a/frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala
+++ b/frontends/benchmarks/imperative/valid/UnfoldOpaqueMutate.scala
@@ -19,12 +19,12 @@ object UnfoldOpaqueMutate {
 
   def test1(wb: WrappedBox, x: BigInt): Unit = {
     @ghost val oldWb = snapshot(wb)
-    unfold(wb.opaqueMutMeth1(x))
+    unfolding(wb.opaqueMutMeth1(x))
     assert(wb.box.cnt == oldWb.box.cnt + x)
   }
 
   def test2(wb: WrappedBox, x: BigInt): Unit = {
-    unfold(wb.opaqueMutMeth2(x))
+    unfolding(wb.opaqueMutMeth2(x))
     assert(wb.box == Box(x * 2))
   }
-}
\ No newline at end of file
+}
diff --git a/frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala b/frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala
index 0f4e4b669..03c1bf866 100644
--- a/frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala
+++ b/frontends/benchmarks/verification/valid/MicroTests/VisibleOpaque.scala
@@ -1,11 +1,11 @@
 import stainless.annotation._
-import stainless.lang.unfold
+import stainless.lang.unfolding
 
 object VisibleOpaque {
   @opaque def p(x: Int) = x > 0
 
   def test(x: Int): Unit = {
-    unfold(p(x))
+    unfolding(p(x))
     assert(p(x) == x > 0)
   }
 }
diff --git a/frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala b/frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala
index e62ba09bb..00323a7bb 100644
--- a/frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala
+++ b/frontends/benchmarks/verification/valid/UnfoldOpaqueVal.scala
@@ -7,7 +7,7 @@ object UnfoldOpaqueVal {
 
   def test(x: BigInt): Unit = {
     val y = opaqueFn(x)
-    unfold(y)
+    unfolding(y)
     assert(y == x + 1)
   }
-}
\ No newline at end of file
+}
diff --git a/frontends/library/stainless/lang/package.scala b/frontends/library/stainless/lang/package.scala
index f019c7449..55fdfa773 100644
--- a/frontends/library/stainless/lang/package.scala
+++ b/frontends/library/stainless/lang/package.scala
@@ -179,7 +179,7 @@ package object lang {
   // typically used when `call` invokes an `opaque` function
   // this adds an equality between the call, and the inlined call
   @library
-  def unfold[T](call: T): Unit = ()
+  def unfolding[T](call: T): Unit = ()
 
   @ignore @library
   implicit class ArrayUpdating[T](a: Array[T]) {