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

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 8265e079e..88af829f8 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -45,6 +45,17 @@
         <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'] 
@@ -70,17 +81,6 @@
         <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,18 +129,7 @@
      </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]"/>