--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:43:26 2014 +0200
@@ -296,8 +296,7 @@
({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : 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,
- live_nesting_bnfs = live_nesting_bnfs, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
- common_co_inducts = common_co_inducts,
+ live_nesting_bnfs = live_nesting_bnfs, maps = maps,
fp_ctr_sugar =
{ctrXs_Tss = ctrXs_Tss,
ctr_defs = ctr_defs,
@@ -306,7 +305,10 @@
{rel_injects = rel_injects,
rel_distincts = rel_distincts},
fp_co_induct_sugar =
- {co_inducts = co_inducts,
+ {co_rec = co_rec,
+ common_co_inducts = common_co_inducts,
+ co_inducts = co_inducts,
+ co_rec_def = co_rec_def,
co_rec_thms = co_rec_thms,
co_rec_discs = co_rec_disc_thms,
co_rec_selss = co_rec_sel_thmss}}