New: expected types (in the sense of Yann Coscoy) now availables for

[helm.git] / helm / style / proofs.xsl

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 5a34d8a06f710fea23eb3a18d494e23174931bc1..1d619260a2dbe6bd22fa5c64d5e14f57b4666081 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -597,7 +597,7 @@
          <m:csymbol>full_or_ind</m:csymbol>
          <xsl:apply-templates mode="noannot" select="*[7]"/>
          <xsl:apply-templates mode="pure" 
-              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>
          <m:apply>
           <m:csymbol>left_case</m:csymbol>
           <m:bvar>
@@ -629,7 +629,7 @@
          <m:csymbol>or_ind</m:csymbol>
          <xsl:apply-templates mode="noannot" select="*[7]"/>
          <xsl:apply-templates mode="pure" 
-              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>
          <xsl:apply-templates mode="pure" select="*[5]"/>
          <xsl:apply-templates mode="pure" select="*[6]"/>
         </m:apply>