--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:34:49 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:35:03 2014 +0200
@@ -296,6 +296,7 @@
({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, ...},
...} : 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,
@@ -327,6 +328,7 @@
co_rec_def = co_rec_def,
co_rec_thms = co_rec_thms,
co_rec_discs = co_rec_disc_thms,
+ co_rec_disc_iffs = co_rec_disc_iffs,
co_rec_selss = co_rec_sel_thmss}}
|> morph_fp_sugar phi;