--- a/src/HOL/Tools/inductive_package.ML Thu Dec 16 12:44:32 2004 +0100
+++ b/src/HOL/Tools/inductive_package.ML Thu Dec 16 14:34:23 2004 +0100
@@ -675,7 +675,7 @@
(*Now break down the individual cases. No disjE here in case
some premise involves disjunction.*)
REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
- ALLGOALS (asm_simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
+ ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
EVERY (map (fn prem =>
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);