--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Oct 24 12:43:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Thu Oct 24 15:32:34 2013 +0200
@@ -155,8 +155,13 @@
REPEAT o (rtac refl ORELSE' atac));
fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
- hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'
- full_simp_tac (ss_only (refl :: no_refl (union Thm.eq_thm discs discs') @ basic_simp_thms) ctxt);
+ let
+ val discs'' = map (perhaps (try (fn th => th RS @{thm notnotD}))) (discs @ discs')
+ |> distinct Thm.eq_thm_prop;
+ in
+ hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'
+ full_simp_tac (ss_only (refl :: no_refl discs'' @ basic_simp_thms) ctxt)
+ end;
fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs
discss selss =