Bug fixed. The bug used to lead to divergence in certain cases (e.g. limit_mul).

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 4c207e4820e6d30f0e52a540aab890478536bc31..7457921334bdc4fa16a3199e714b0c785b18ae40 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -510,7 +510,7 @@
       <m:csymbol>side_proof</m:csymbol>
      </xsl:otherwise>
     </xsl:choose>
-    <xsl:apply-templates mode="proof_transform" select="."/>
+    <xsl:apply-templates mode="proof_transform" select="$proof"/>
     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
    </m:apply>
    <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->