Temporary patch for threads and and_ind, or_ind, ...

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 88af829f8eadf6c14521fd64947e512503cd0bef..8265e079e261615fe0dc374c51001dbd551160e7 100644 (file)
--- 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]"/>