diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index b4866c39921c1e7c6feddcc9af1668522d4ae844..0c158ec3225c6b136357daff92667dddfbce3e86 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1185,11 +1185,9 @@ object ExprOps {
     }
 
     def traverse(funDef: FunDef): Seq[T] = {
-      // @mk FIXME: This seems overly compicated
-      val precondition = funDef.precondition.map(e => matchToIfThenElse(e)).toSeq
-      val precTs = funDef.precondition.map(e => traverse(e)).toSeq.flatten
-      val bodyTs = funDef.body.map(e => traverse(e, precondition)).toSeq.flatten
-      val postTs = funDef.postcondition.map(p => traverse(p)).toSeq.flatten
+      val precTs = funDef.precondition.toSeq.flatMap(traverse)
+      val bodyTs = funDef.body.toSeq.flatMap(traverse(_, funDef.precondition.toSeq))
+      val postTs = funDef.postcondition.toSeq.flatMap(traverse)
       precTs ++ bodyTs ++ postTs
     }