# HG changeset patch
# User paulson
# Date 1033737838 -7200
# Node ID 67b0b7500a9dbde470f58ffc626b684b993adf04
# Parent  282fbabec8625daf44bbef75f77f3423f18f53e8
Fixed bug involving inductive definitions with equalities in the premises.

diff -r 282fbabec862 -r 67b0b7500a9d src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Oct 04 15:23:12 2002 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Fri Oct 04 15:23:58 2002 +0200
@@ -323,7 +323,8 @@
        Intro rules with extra Vars in premises still cause some backtracking *)
      fun ind_tac [] 0 = all_tac
        | ind_tac(prem::prems) i =
-             DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN
+             DEPTH_SOLVE_1 (ares_tac [prem, refl] i APPEND hyp_subst_tac i) 
+             THEN
              ind_tac prems (i-1);
 
      val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
@@ -362,8 +363,7 @@
              REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
              (*Now break down the individual cases.  No disjE here in case
                some premise involves disjunction.*)
-             REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE]
-                                ORELSE' hyp_subst_tac)),
+             REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE])),
              ind_tac (rev prems) (length prems) ]);
 
      val dummy = if !Ind_Syntax.trace then