# HG changeset patch
# User blanchet
# Date 1379511210 -7200
# Node ID a3ad5a0350f909c49a59c9f052c7b019b950e7cb
# Parent  705f0b728b1b67b957a077c35ba3a4426d1ad47c
avoid duplicate simp rule warnings

diff -r 705f0b728b1b -r a3ad5a0350f9 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Wed Sep 18 12:16:10 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Wed Sep 18 15:33:30 2013 +0200
@@ -156,7 +156,7 @@
 
 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 (discs @ discs') @ basic_simp_thms) ctxt);
+  full_simp_tac (ss_only (refl :: no_refl (union Thm.eq_thm discs discs') @ basic_simp_thms) ctxt);
 
 fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs
     discss selss =