# HG changeset patch
# User blanchet
# Date 1420437375 -3600
# Node ID c6f2867e743f5b139dda8af4a857314f8f0ce259
# Parent  c448752e8b9d4103713b9a071da2d7e42ab92826
tuning

diff -r c448752e8b9d -r c6f2867e743f src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 19 11:18:58 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Jan 05 06:56:15 2015 +0100
@@ -234,8 +234,8 @@
 val case_eq_ifN = "case_eq_if";
 val collapseN = "collapse";
 val discN = "disc";
+val disc_eq_caseN = "disc_eq_case";
 val discIN = "discI";
-val disc_eq_caseN = "disc_eq_case";
 val distinctN = "distinct";
 val distinct_discN = "distinct_disc";
 val exhaustN = "exhaust";
@@ -990,9 +990,9 @@
 
               val disc_eq_case_thms =
                 let
-                  fun term_of_bool b = if b then @{term True} else @{term False};
+                  fun const_of_bool b = if b then @{const True} else @{const False};
                   fun mk_case_args n = map_index (fn (k, argTs) =>
-                    fold_rev Term.absdummy argTs (term_of_bool (n = k))) ctr_Tss;
+                    fold_rev Term.absdummy argTs (const_of_bool (n = k))) ctr_Tss;
                   val goals = map_index (fn (n, udisc) =>
                     mk_Trueprop_eq (udisc, list_comb (casexBool, mk_case_args n) $ u)) udiscs;
                 in
@@ -1047,8 +1047,8 @@
            (case_eq_ifN, case_eq_if_thms, []),
            (collapseN, safe_collapse_thms, if ms = [0] then [] else simp_attrs),
            (discN, flat nontriv_disc_thmss, simp_attrs),
+           (disc_eq_caseN, disc_eq_case_thms, []),
            (discIN, nontriv_discI_thms, []),
-           (disc_eq_caseN, disc_eq_case_thms, []),
            (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
            (distinct_discN, distinct_disc_thms, dest_attrs),
            (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),