<xsl:when test="name()='APPLY'">
<xsl:variable name="id" select="@id"/>
<xsl:choose>
- <xsl:when test="name(*[1])='CONST'">
+ <xsl:when test="name(*[1])='CONST' or
+ (name(*[1])='instantiate' and name(*[1]/*[1])='CONST')">
<xsl:apply-templates mode="try_inductive" select="."/>
</xsl:when>
<!-- patch temporanea per la gestione di redex -->
</m:ci>
</m:bvar>
<xsl:apply-templates mode="noannot" select="*[2]"/>
- <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
+ <xsl:apply-templates mode="lambda_prop" select="*[1]/*[2]"/>
</m:apply>
</xsl:when>
<xsl:otherwise>