src/HOL/Tools/inductive_package.ML
changeset 22980 1226d861eefb
parent 22846 fb79144af9a3
child 22997 d4f3b015b50b
--- 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