X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=01b2a41cbaff49ddb6c220179e3eda48ea6754c4;hb=4df1801e4b86a7ab64211b65e8072adcb7787c62;hp=2570adc7381dca131c45e76f09f70fcfe2ed808c;hpb=ddce32beebecf9d965e6ad991a08368f52cd9ea1;p=helm.git

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 2570adc73..01b2a41cb 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -2136,8 +2136,6 @@ CONJECTURES:
           <xsl:with-param name="current_indent" select="$current_indent"/>
          </xsl:apply-templates>
         </xsl:when>
-       </xsl:choose>
-       <xsl:choose>
         <xsl:when test="name(.)='Def'">
          <xsl:choose>
           <xsl:when test="@name">
@@ -2152,10 +2150,10 @@ CONJECTURES:
           <xsl:with-param name="current_indent" select="$current_indent"/>
          </xsl:apply-templates>
         </xsl:when>
+        <xsl:otherwise>
+         <xsl:text> _ :? _ </xsl:text>
+        </xsl:otherwise>
        </xsl:choose>
-       <xsl:otherwise>
-        <xsl:text> _ :? _ </xsl:text>
-       </xsl:otherwise>
       </xsl:for-each>
       |- <xsl:value-of select="./@no"/> : 
       <xsl:apply-templates select="./Goal/*[1]">