* getter.xsl added

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

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 51a0f0d52a5abc6b91eff213af41aeaf01049061..0651f65ec6cdb2224b864010bd8a5025953cbee2 100644 (file)
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -108,8 +108,9 @@
       <xsl:when test="contains($uri,'_ind.con')">
        <xsl:variable name="ind_uri" 
          select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
+       <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
        <xsl:variable name="inductive_def" 
-     select="document(concat(string($absPath),$ind_uri))/InductiveDefinition"/>
+     select="document($InductiveTypeUrl)/InductiveDefinition"/>
        <!-- check if the corresponding inductive definition actually
             exists -->
        <xsl:choose>