src/HOL/Tools/inductive_package.ML
changeset 13747 bf308fcfd08e
parent 13709 ec00ba43aee8
child 14235 281295a1bbaa
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 12 11:33:48 2002 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 12 11:38:18 2002 +0100
     1.3 @@ -675,11 +675,10 @@
     1.4           REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
     1.5           (*Now break down the individual cases.  No disjE here in case
     1.6             some premise involves disjunction.*)
     1.7 -         REPEAT (FIRSTGOAL (etac conjE)),
     1.8 +         REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
     1.9           ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
    1.10           EVERY (map (fn prem =>
    1.11 -			DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1 APPEND 
    1.12 -						hyp_subst_tac 1)) prems)]);
    1.13 +   	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    1.14  
    1.15      val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
    1.16        (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>