src/HOL/Tools/BNF/bnf_lfp_compat.ML
changeset 57794 73052169b213
parent 57633 4ff8c090d580
child 57798 018dc778cbcc
equal deleted inserted replaced
57793:d1cf76cef93b 57794:73052169b213
   122 
   122 
   123     fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
   123     fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
   124         distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
   124         distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
   125       (T_name0,
   125       (T_name0,
   126        {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
   126        {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
   127        inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
   127         inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
   128        rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
   128         rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
   129        case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
   129         case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
   130        split_asm = split_asm});
   130         split_asm = split_asm});
   131 
   131 
   132     val infos = map_index mk_info (take nn_fp fp_sugars);
   132     val infos = map_index mk_info (take nn_fp fp_sugars);
   133 
   133 
   134     val all_notes =
   134     val all_notes =
   135       (case lfp_sugar_thms of
   135       (case lfp_sugar_thms of