Code clean-up: the widget in the lower-left corner is now a widget to input

[helm.git] / helm / style / objcontent.xsl
diff --git a/helm/style/objcontent.xsl b/helm/style/objcontent.xsl

index 9cf2ca7f9fb5b4437345c57cd300355039460b8b..405529785fea3c6db83485369e4eb5837a11f832 100644 (file)
--- a/helm/style/objcontent.xsl
+++ b/helm/style/objcontent.xsl
@@ -158,7 +158,9 @@
       <body>
        <xsl:apply-templates select="./*[1]"/>
       </body>
-     <type/>
+     <type>
+       <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
+     </type>
      </Definition>
  </xsl:template>
  
@@ -169,7 +171,7 @@
        <Conjecture no="{@no}" helm:xref="{@id}">
          <xsl:for-each select="*">
           <xsl:copy>
-          <xsl:copy-of select="@of"/>
+          <xsl:copy-of select="@name"/>
            <xsl:attribute name="helm:xref">
             <xsl:value-of select="@id"/>
            </xsl:attribute>
@@ -181,6 +183,9 @@
       <body>
         <xsl:apply-templates select="body/*[1]"/>
       </body>
+     <type>
+       <xsl:apply-templates select="document($ConstantTypeUrl)/*[1]/*[1]"/>
+     </type>
      </CurrentProof> 
  </xsl:template>