diff -r 9cd12369e753 -r 5d523a1b6ddc src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Apr 07 12:48:10 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Apr 07 17:27:53 2006 +0200
@@ -661,7 +661,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 (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
+         rewrite_goals_tac sum_case_rewrites,
          EVERY (map (fn prem =>
            DEPTH_SOLVE_1 (ares_tac [rewrite_rule [inductive_conj_def] prem, conjI, refl] 1)) prems)]));