# HG changeset patch
# User berghofe
# Date 1179246007 -7200
# Node ID 1226d861eefb5804236c17779261bc6c5cda4fc7
# Parent  d95580341be5941088541b7d61928eb86414b5fb
Fixed bug that caused proof of induction theorem to fail if
introduction rules contained True or False.

diff -r d95580341be5 -r 1226d861eefb src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue May 15 08:10:31 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue May 15 18:20:07 2007 +0200
@@ -550,7 +550,8 @@
          REPEAT (FIRSTGOAL
            (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
-           (inductive_conj_def :: rec_preds_defs) prem, conjI, refl] 1)) prems)]);
+             (inductive_conj_def :: rec_preds_defs @ simp_thms') prem,
+           conjI, refl] 1)) prems)]);
 
     val lemma = SkipProof.prove ctxt'' [] []
       (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY