<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']
<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>
</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]"/>