Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid duplicate simp rule warnings
authorblanchet
Wed, 18 Sep 2013 15:33:30 +0200
changeset 53690 a3ad5a0350f9
parent 53689 705f0b728b1b
child 53691 fa103abdbade
avoid duplicate simp rule warnings
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle