From 56e7429421ba1264c40e4f7d00bf1c038ece6f80 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 6 Dec 2002 16:05:48 +0000
Subject: [PATCH] instantiate for inductive principles covered

---
 helm/style/proofs.xsl | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 65de766d1..6f49a2678 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -237,7 +237,8 @@
   <xsl:when test="name()='APPLY'">
    <xsl:variable name="id" select="@id"/>
    <xsl:choose>
-    <xsl:when test="name(*[1])='CONST'">
+    <xsl:when test="name(*[1])='CONST' or 
+      (name(*[1])='instantiate' and name(*[1]/*[1])='CONST')">
      <xsl:apply-templates mode="try_inductive" select="."/>
     </xsl:when>
     <!-- patch temporanea per la gestione di redex -->
-- 
2.39.2