src/HOL/Tools/Datatype/datatype_data.ML
changeset 57983 6edc3529bb4e
parent 56858 0c3d0bc98abe
child 58111 82db9ad610b9
     1.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4    head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of case_rewrite))));
     1.5  
     1.6  fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
     1.7 -    weak_case_cong, split, split_asm, ...} : Datatype_Aux.info) =
     1.8 +    case_cong_weak, split, split_asm, ...} : Datatype_Aux.info) =
     1.9    {ctrs = ctrs_of_exhaust exhaust,
    1.10     casex = case_of_case_rewrite (hd case_rewrites),
    1.11     discs = [],
    1.12 @@ -106,7 +106,7 @@
    1.13     distincts = distinct,
    1.14     case_thms = case_rewrites,
    1.15     case_cong = case_cong,
    1.16 -   weak_case_cong = weak_case_cong,
    1.17 +   case_cong_weak = case_cong_weak,
    1.18     split = split,
    1.19     split_asm = split_asm,
    1.20     disc_defs = [],
    1.21 @@ -114,13 +114,13 @@
    1.22     discIs = [],
    1.23     sel_defs = [],
    1.24     sel_thmss = [],
    1.25 -   disc_excludesss = [],
    1.26 -   disc_exhausts = [],
    1.27 -   sel_exhausts = [],
    1.28 +   distinct_discsss = [],
    1.29 +   exhaust_discs = [],
    1.30 +   exhaust_sels = [],
    1.31     collapses = [],
    1.32     expands = [],
    1.33 -   sel_splits = [],
    1.34 -   sel_split_asms = [],
    1.35 +   split_sels = [],
    1.36 +   split_sel_asms = [],
    1.37     case_eq_ifs = []};
    1.38  
    1.39  fun register dt_infos =