--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 12 16:08:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 12 16:51:55 2016 +0200
@@ -685,7 +685,7 @@
val (ctr_sugar as {case_cong, ...}, lthy) =
free_constructors (ctr_sugar_kind_of_fp_kind fp) tacss
- ((((plugins, discs_sels), standard_binding), ctr_specs), sel_default_eqs) lthy
+ ((((plugins, discs_sels), standard_binding), ctr_specs), sel_default_eqs) lthy;
val anonymous_notes =
[([case_cong], fundefcong_attrs)]
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Sep 12 16:08:27 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Sep 12 16:51:55 2016 +0200
@@ -872,7 +872,8 @@
exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
val nontriv_disc_defs = disc_defs
- |> filter_out (member Thm.eq_thm_prop [unique_disc_no_def, alternate_disc_no_def]);
+ |> filter_out (member Thm.eq_thm_prop [unique_disc_no_def, alternate_disc_no_def,
+ refl]);
val disc_defs' =
map2 (fn k => fn def =>