--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:35:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:35:29 2014 +0200
@@ -296,7 +296,8 @@
({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, ...},
fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels,
rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases, ...},
- fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, ...},
+ fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
+ common_rel_co_inducts, ...},
...} : fp_sugar) =
{T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
@@ -331,7 +332,8 @@
co_rec_disc_iffs = co_rec_disc_iffs,
co_rec_selss = co_rec_sel_thmss,
co_rec_codes = co_rec_codes,
- co_rec_transfers = co_rec_transfers}}
+ co_rec_transfers = co_rec_transfers,
+ common_rel_co_inducts = common_rel_co_inducts}}
|> morph_fp_sugar phi;
val target_fp_sugars =