X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fproofs.xsl;h=69c8936130bcaf605a2f28956b438226c9cacec5;hb=911199dc198f34ae6a024d81ff62c78e2e97f7db;hp=65de766d1bb65d787267518f7509cd57a92fcdfc;hpb=1898ffc8283cf32f9551c6cce80b43e6355a4579;p=helm.git

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 65de766d1..69c893613 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -237,7 +237,8 @@
   <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 -->
@@ -256,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>