--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:33:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:33:24 2014 +0200
@@ -294,7 +294,7 @@
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
({fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels,
- rel_intros, ...}, ...} : fp_sugar) =
+ rel_intros, rel_cases, ...}, ...} : 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,
@@ -309,7 +309,8 @@
rel_injects = rel_injects,
rel_distincts = rel_distincts,
rel_sels = rel_sels,
- rel_intros = rel_intros},
+ rel_intros = rel_intros,
+ rel_cases = rel_cases},
fp_co_induct_sugar =
{co_rec = co_rec,
common_co_inducts = common_co_inducts,