removed spurious "simp"
authorblanchet
Wed, 18 Sep 2013 18:56:48 +0200
changeset 548380643a443bb63
parent 54837 e6a44d775be3
child 54839 9b034e6b977c
removed spurious "simp"
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Sep 18 18:53:24 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Sep 18 18:56:48 2013 +0200
     1.3 @@ -1034,7 +1034,7 @@
     1.4      ((coinduct_thms_pairs, coinduct_case_attrs),
     1.5       (unfold_thmss, corec_thmss, []),
     1.6       (safe_unfold_thmss, safe_corec_thmss),
     1.7 -     (disc_unfold_thmss, disc_corec_thmss, simp_attrs),
     1.8 +     (disc_unfold_thmss, disc_corec_thmss, []),
     1.9       (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
    1.10       (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
    1.11    end;