X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Finductive.xsl;h=83569d751660cf0008629f29c8986d149b2f0441;hb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;hp=5211c000c8e3de2f684f0571d97d9e6e3e10939a;hpb=0a3a47d4b47605d55010bc2ef1175e8562bbdec2;p=helm.git

diff --git a/helm/style/inductive.xsl b/helm/style/inductive.xsl
index 5211c000c..83569d751 100644
--- 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>
-