# HG changeset patch
# User blanchet
# Date 1382621554 -7200
# Node ID 4fadf746f2d512b9ba71beb8713fb45f56746903
# Parent  994ebb795b752707c46eb7ca9a40491efb2cea1f
got rid of annoying duplicate rewrite rule warnings

diff -r 994ebb795b75 -r 4fadf746f2d5 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- 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 =