# HG changeset patch
# User berghofe
# Date 1144423673 -7200
# Node ID 5d523a1b6ddc2cbc483827f5c879cded191c19b3
# Parent  9cd12369e753ba3fc233d9cc174d22a57bfd888d
Fixed bug that caused proof of induction rule to fail
for inductive sets with trivial introduction rules
such as "x : S ==> x : S".

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