# HG changeset patch
# User paulson
# Date 1039689498 -3600
# Node ID bf308fcfd08ecc5c643f38b55da08ee243f937ce
# Parent  550260ace09e13dc0fddd4f712d7a0bcd20f76c8
Better treatment of equality in premises of inductive definitions.  Less
backtracking.

diff -r 550260ace09e -r bf308fcfd08e src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Dec 12 11:33:48 2002 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 12 11:38:18 2002 +0100
@@ -675,11 +675,10 @@
          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
          (*Now break down the individual cases.  No disjE here in case
            some premise involves disjunction.*)
-         REPEAT (FIRSTGOAL (etac conjE)),
+         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
          ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
          EVERY (map (fn prem =>
-			DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1 APPEND 
-						hyp_subst_tac 1)) prems)]);
+   	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
 
     val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
diff -r 550260ace09e -r bf308fcfd08e src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Dec 12 11:33:48 2002 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Thu Dec 12 11:38:18 2002 +0100
@@ -323,9 +323,7 @@
        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 APPEND hyp_subst_tac i) 
-             THEN
-             ind_tac prems (i-1);
+             DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN ind_tac prems (i-1);
 
      val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
 
@@ -363,7 +361,8 @@
              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])),
+             REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE]
+	                        ORELSE' bound_hyp_subst_tac)),
              ind_tac (rev prems) (length prems) ]);
 
      val dummy = if !Ind_Syntax.trace then