src/ZF/Tools/inductive_package.ML

 
      (*Minimizes backtracking by delivering the correct premise to each goal.
        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);
 
      val ind_prems = map (induct_prem (map (rpair pred) rec_tms))

              full_simp_tac (min_ss addsimps [Part_Collect]) 1,
              (*This CollectE and disjE separates out the introduction rules*)
              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
                  (writeln "quant_induct = "; print_thm quant_induct)
              else ();