1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Wed Sep 18 12:16:10 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Wed Sep 18 15:33:30 2013 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4  
     1.5  fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
     1.6    hyp_subst_tac ctxt THEN' REPEAT o etac conjE THEN'
     1.7 -  full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms) ctxt);
     1.8 +  full_simp_tac (ss_only (refl :: no_refl (union Thm.eq_thm discs discs') @ basic_simp_thms) ctxt);
     1.9  
    1.10  fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs
    1.11      discss selss =