src/HOL/Tools/record.ML
changeset 57983 6edc3529bb4e
parent 57225 ff69e42ccf92
child 58187 d2ddd401d74d
     1.1 --- a/src/HOL/Tools/record.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -1785,10 +1785,10 @@
     1.4    Ctr_Sugar.default_register_ctr_sugar_global T_name
     1.5      {ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels], exhaust = exhaust,
     1.6       nchotomy = Drule.dummy_thm, injects = [inject], distincts = [], case_thms = [],
     1.7 -     case_cong = Drule.dummy_thm, weak_case_cong = Drule.dummy_thm, split = Drule.dummy_thm,
     1.8 +     case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm, split = Drule.dummy_thm,
     1.9       split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [], discIs = [], sel_defs = sel_defs,
    1.10 -     sel_thmss = [sel_thms], disc_excludesss = [], disc_exhausts = [], sel_exhausts = [],
    1.11 -     collapses = [], expands = [], sel_splits = [], sel_split_asms = [], case_eq_ifs = []};
    1.12 +     sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [], exhaust_sels = [],
    1.13 +     collapses = [], expands = [], split_sels = [], split_sel_asms = [], case_eq_ifs = []};
    1.14  
    1.15  
    1.16  (* definition *)