diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index 3b80989e6f70f893b86bedaaf7632823e9015159..fadab3b73314474dcb6cbb77c8d6e25df04aa105 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -77,7 +77,10 @@ object AntiAliasingPhase extends TransformationPhase {
     }.map(_.id)
 
     val newParams = fd.params.map(vd => vd.getType match {
-      case (ft: FunctionType) => ValDef(vd.id.duplicate(tpe = makeFunctionTypeExplicit(ft)))
+      case (ft: FunctionType) => {
+        val nft = makeFunctionTypeExplicit(ft)
+        if(ft == nft) vd else ValDef(vd.id.duplicate(tpe = nft))
+      }
       case _ => vd
     })
 
diff --git a/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams7.scala b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b32043f0095c52189fadb8765ea744ab746f8d0a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/HigherOrderFunctionsMutableParams7.scala
@@ -0,0 +1,19 @@
+object HigherOrderFunctionsMutableParams7 {
+  /*
+   * this test catches an error that happened in
+   * xlang when renaming higher order functions parameter
+   * even though the function had a pure signature (Int => Int)
+   */
+
+  def app(f: (Int) => Int, x: Int): Int = {
+    f(x)
+  }
+
+  def id(x: Int) = x
+
+  def test(): Int = {
+    val x = 12
+    app(id, 12)
+  } ensuring(_ == 12)
+
+}