# HG changeset patch
# User blanchet
# Date 1473691915 -7200
# Node ID d0e8921da31193948a0b8abc2cbc8b2f97e608c3
# Parent  0a6b145879f4ec83713d67a0011527f44e86db72
avoid warning triggered by code generator

diff -r 0a6b145879f4 -r d0e8921da311 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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)]
diff -r 0a6b145879f4 -r d0e8921da311 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- 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 =>