X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fcontent_to_html.xsl;h=5a48cc1ea49933cc3b3d492a119822d5c07f8353;hb=3f40909b16020098d481eb0c8814c56e26865bf1;hp=71a82f613d16be524a61c0eb1c75febbf2e0945f;hpb=03d580b649e5e3cfdb1df8640ffc66c1915695c2;p=helm.git

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 71a82f613..5a48cc1ea 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -733,6 +733,23 @@
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <xsl:when test="$name='let_in'">
+       <xsl:text>let&#x00a0;</xsl:text>
+       <xsl:apply-templates select="m:bvar/m:ci"/>
+       <xsl:text>&#x00a0;:=&#x00a0;</xsl:text>
+       <xsl:apply-templates select="*[3]">
+        <xsl:with-param name="current_indent" select="$current_indent+14"/>
+       </xsl:apply-templates>
+       <br/>
+       <xsl:call-template name="make_indent">
+        <xsl:with-param name="current_indent" select="$current_indent"/> 
+       </xsl:call-template>
+       <xsl:text>in&#x00a0;</xsl:text>
+       <xsl:apply-templates select="*[4]">
+        <xsl:with-param name="current_indent" select="$current_indent+5"/>
+       </xsl:apply-templates>
+      </xsl:when>
+
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
       <!-- ***************************************** -->
@@ -1190,7 +1207,7 @@
       <!-- *********** LAMBDA ELEMENTS ************** -->
       <!-- ***************************************** -->
       <xsl:when test="$name='subst'">
-       <xsl:apply-templates select="*[2]"/>
+       <xsl:apply-templates select="*[3]"/>
        <xsl:text>[</xsl:text>
        <xsl:apply-templates select="*[4]"/>
        <a href="{*[1]/@definitionURL}">
@@ -1198,7 +1215,7 @@
         <xsl:text>&#x00ac;</xsl:text>
        </FONT>
        </a>
-       <xsl:apply-templates select="*[3]"/>
+       <xsl:apply-templates select="*[2]"/>
        <xsl:text>]</xsl:text>
       </xsl:when>