X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fproofs.xsl;h=8265e079e261615fe0dc374c51001dbd551160e7;hb=51a083ff0a97be71d2748d41c9a526eb839e9c2c;hp=88af829f8eadf6c14521fd64947e512503cd0bef;hpb=413a5e0b1fde6296a09a6651cef7948bc408c6e4;p=helm.git

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 88af829f8..8265e079e 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -45,17 +45,6 @@
         <xsl:apply-templates mode="thread" select="*[5]"/>
        </m:apply>
       </xsl:when>
-      <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
-       <m:apply helm:xref="{@id}">
-        <m:csymbol>thread</m:csymbol>
-        <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
-        <m:apply>
-         <m:csymbol>app</m:csymbol>
-         <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
-        </m:apply>
-        <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
-       </m:apply>
-      </xsl:when>
       <!-- aggiungere la verifica dell'esistenza dei lambda per and_ind -->
       <xsl:when test="name()= 'APPLY' and CONST[
  attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con'] 
@@ -81,6 +70,17 @@
         <xsl:apply-templates mode="pure" select="*[6]"/>
        </m:apply>
       </xsl:when>
+      <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
+       <m:apply helm:xref="{@id}">
+        <m:csymbol>thread</m:csymbol>
+        <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>
+        <m:apply>
+         <m:csymbol>app</m:csymbol>
+         <xsl:apply-templates mode="copy-of-no-prop" select="*[1]"/>
+        </m:apply>
+        <xsl:apply-templates mode="thread" select="*[@id = //ALLTYPES/TYPE/@id]"/>
+       </m:apply>
+      </xsl:when>
       <xsl:otherwise>
        <m:apply helm:xref="{@id}">
         <m:csymbol>proof</m:csymbol>
@@ -129,7 +129,18 @@
      </m:apply>
      <xsl:apply-templates mode="thread" select="*[5]"/>
    </xsl:when>
+<!--**** Patch temporanea, per il problema dei threads ***-->
+<xsl:when test="(name()= 'APPLY' and CONST[
+ attribute::uri='cic:/coq/INIT/Logic/Conjunction/and_ind.con'] 
+ and count(child::*) = 6) or
+(name()= 'APPLY' and CONST[
+ attribute::uri='cic:/coq/INIT/Logic/Disjunction/or_ind.con'] 
+ and count(child::*) = 7)">
+ <xsl:apply-templates mode="noannot" select="."/>
+</xsl:when>
+<!--**** Fine Patch temporanea, per il problema dei threads ***-->
    <xsl:when test="count(*[@id = //ALLTYPES/TYPE/@id]) = 1">
+       <xsl:variable name="id" select="@id"/>
        <m:apply helm:xref="{@id}">
         <m:csymbol>thread</m:csymbol>
         <xsl:apply-templates mode="pure" select="//ALLTYPES/TYPE[@id=$id]"/>