Bug nat_double_ind solved.

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

diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index 5211c000c8e3de2f684f0571d97d9e6e3e10939a..f9b535f1e72e43a60299b80ed5da5494d51064ca 100644 (file)
--- a/helm/style/inductive.xsl
+++ b/helm/style/inductive.xsl
@@ -36,7 +36,8 @@
 
 
 <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"/>
@@ -63,9 +64,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"/>