Bug fixed: beta-redex transformations to LetIn were bugged when the lambda

had two or more decls.

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 6f49a2678db95f6c33454fb75819f42db5a4015e..69c8936130bcaf605a2f28956b438226c9cacec5 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -257,7 +257,7 @@
        </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>