avoid warning triggered by code generator
authorblanchet
Mon, 12 Sep 2016 16:51:55 +0200
changeset 63853 d0e8921da311
parent 63852 0a6b145879f4
child 63854 e90f51b20215
avoid warning triggered by code generator
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_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)]
--- 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 =>