Fixed bug that caused proof of induction rule to fail
for inductive sets with trivial introduction rules
such as "x : S ==> x : S".

--- 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)]));