# HG changeset patch
# User blanchet
# Date 1466191559 -7200
# Node ID 0c956a9a0ac048ee948bde87eac892d9717adcf3
# Parent  d75d1e399698f42df65ab871b30405d5c48046fd
avoid runtime warning with discriminators due to 'Code.del_eqn'

diff -r d75d1e399698 -r 0c956a9a0ac0 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jun 17 21:00:32 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Jun 17 21:25:59 2016 +0200
@@ -805,12 +805,13 @@
             (thm, asm_thm)
           end;
 
-        val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
-             discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
-             exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms,
-             expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms, disc_eq_case_thms) =
+        val (sel_defs, all_sel_thms, sel_thmss, disc_defs, nontriv_disc_defs, disc_thmss,
+             nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms,
+             distinct_disc_thmsss, exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms,
+             safe_collapse_thms, expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms,
+             disc_eq_case_thms) =
           if no_discs_sels then
-            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
+            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
           else
             let
               val udiscs = map (rapp u) discs;
@@ -870,6 +871,9 @@
               val has_alternate_disc_def =
                 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]);
+
               val disc_defs' =
                 map2 (fn k => fn def =>
                   if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
@@ -1044,11 +1048,11 @@
                   |> Conjunction.elim_balanced (length goals)
                 end;
             in
-              (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss,
-               discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss,
-               [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms,
-               [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm],
-               disc_eq_case_thms)
+              (sel_defs, all_sel_thms, sel_thmss, disc_defs, nontriv_disc_defs, disc_thmss,
+               nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms,
+               distinct_disc_thmsss, [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms,
+               safe_collapse_thms, [expand_thm], [split_sel_thm], [split_sel_asm_thm],
+               [case_eq_if_thm], disc_eq_case_thms)
             end;
 
         val case_distrib_thm =
@@ -1118,7 +1122,7 @@
           |> Local_Theory.declaration {syntax = false, pervasive = true}
             (fn phi => Case_Translation.register
                (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
-          |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
+          |> Local_Theory.background_theory (fold (fold Code.del_eqn) [nontriv_disc_defs, sel_defs])
           |> plugins code_plugin ?
             Local_Theory.declaration {syntax = false, pervasive = false}
               (fn phi => Context.mapping
@@ -1135,7 +1139,7 @@
            exhaust = exhaust_thm, nchotomy = nchotomy_thm, injects = inject_thms,
            distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm,
            case_cong_weak = case_cong_weak_thm, case_distribs = [case_distrib_thm],
-           split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
+           split = split_thm, split_asm = split_asm_thm, disc_defs = nontriv_disc_defs,
            disc_thmss = disc_thmss, discIs = discI_thms, disc_eq_cases = disc_eq_case_thms,
            sel_defs = sel_defs, sel_thmss = sel_thmss, distinct_discsss = distinct_disc_thmsss,
            exhaust_discs = exhaust_disc_thms, exhaust_sels = exhaust_sel_thms,