# HG changeset patch
# User blanchet
# Date 1379523408 -7200
# Node ID 0643a443bb630fe211c064ef81636a3f7ff0d205
# Parent  e6a44d775be396a89b2156cad6fea370c6a81808
removed spurious "simp"

diff -r e6a44d775be3 -r 0643a443bb63 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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;