diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala index 0f47e61ac0e8fa4d373e287f87160fd98e57673b..05648fc9fc14608b7321ffd4f341cb5467a88d01 100644 --- a/src/main/scala/leon/utils/TypingPhase.scala +++ b/src/main/scala/leon/utils/TypingPhase.scala @@ -61,7 +61,11 @@ object TypingPhase extends LeonPhase[Program, Program] { ).setPos(p)).setPos(p)) case None => - Some(Lambda(Seq(ValDef(resId)), IsInstanceOf(ct, Variable(resId)))) + val pos = fd.body.map{ _.getPos } match { + case Some(df: DefinedPosition) => df.focusEnd + case _ => NoPosition + } + Some(Lambda(Seq(ValDef(resId)), IsInstanceOf(ct, Variable(resId))).setPos(pos)) } } case _ => fd.postcondition