- the mathql interpreter is not helm-dependent any more

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

diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index 5211c000c8e3de2f684f0571d97d9e6e3e10939a..83569d751660cf0008629f29c8986d149b2f0441 100644 (file)
--- a/helm/style/inductive.xsl
+++ b/helm/style/inductive.xsl
@@ -36,14 +36,16 @@
 
 
 <xsl:template mode="inductive" match="APPLY">
- <xsl:param name="inductive_def_uri" select="/.."/>
+ <xsl:param name="inductive_def_uri" select="''"/>
+ <xsl:param name="inductive_def" select="/.."/>
  <xsl:param name="inductive_def_index" select="1"/>
  <xsl:param name="inductive_def_name" select="''"/>
  <xsl:param name="section_params" select="0"/>
  <!-- expected_args_type contains the types of the arguments expected by
       the induction principle -->
+ <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="*[1]/@uri"/></xsl:call-template></xsl:variable>
  <xsl:variable name="expected_args_types" 
-       select="document(concat(string($absPath),*[1]/@uri))/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
+       select="document($InductiveTypeUrl)/Definition/type//PROD[not(ancestor::source)]/source/*[1]"/>
  <xsl:variable name="no_expected_args" select="count($expected_args_types)"/>
  <xsl:variable name="actual_arguments" select="*[position()>(1+$section_params)]"/>
  <!-- First check that the induction principle is applied to the
@@ -63,9 +65,6 @@
     <xsl:when test="string($argsOK) = 'true'">
      <!-- arguments are in the expected form: we create a
           "by_induction" content element -->
-     <!-- inductive_def contains the inductive definition -->
-     <xsl:variable name="inductive_def" 
-      select="document(concat(string($absPath),$inductive_def_uri))/InductiveDefinition"/>
      <!-- no_params is the number of paramters in square brackets -->
      <xsl:variable name="no_params" 
       select="$inductive_def/@noParams"/>
@@ -405,6 +404,4 @@
  </xsl:choose>
 </xsl:template>
 
-
 </xsl:stylesheet>
-