src/HOL/Tools/inductive_package.ML
changeset 15416 db69af736ebb
parent 15391 797ed46d724b
child 15463 95cb3eb74307
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 16 12:44:32 2004 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 16 14:34:23 2004 +0100
     1.3 @@ -675,7 +675,7 @@
     1.4           (*Now break down the individual cases.  No disjE here in case
     1.5             some premise involves disjunction.*)
     1.6           REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
     1.7 -         ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
     1.8 +         ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
     1.9           EVERY (map (fn prem =>
    1.10     	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    1.11