src/HOL/Tools/BNF/bnf_lfp_compat.ML
changeset 57983 6edc3529bb4e
parent 57807 5b9043595b7d
child 58112 8081087096ad
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -138,12 +138,12 @@
     1.4      val inducts = map (the_single o #co_inducts) fp_sugars;
     1.5  
     1.6      fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
     1.7 -        distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
     1.8 +        distincts, case_thms, case_cong, case_cong_weak, split, split_asm, ...}, ...} : fp_sugar) =
     1.9        (T_name0,
    1.10         {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
    1.11          inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
    1.12          rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
    1.13 -        case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
    1.14 +        case_cong = case_cong, case_cong_weak = case_cong_weak, split = split,
    1.15          split_asm = split_asm});
    1.16  
    1.17      val infos = map_index mk_info (take nn_fp fp_sugars);