src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 53701 0643a443bb63
parent 53694 7b453b619b5f
child 53741 c9068aade859
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Sep 18 18:53:24 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Sep 18 18:56:48 2013 +0200
@@ -1034,7 +1034,7 @@
     ((coinduct_thms_pairs, coinduct_case_attrs),
      (unfold_thmss, corec_thmss, []),
      (safe_unfold_thmss, safe_corec_thmss),
-     (disc_unfold_thmss, disc_corec_thmss, simp_attrs),
+     (disc_unfold_thmss, disc_corec_thmss, []),
      (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
      (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
   end;