--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:32:53 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:33:04 2014 +0200
@@ -293,7 +293,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, ...}, ...} : fp_sugar) =
+ ({fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels, ...}, ...} : 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,
@@ -306,7 +306,8 @@
map_disc_iffs = map_disc_iffs,
map_sels = map_sels,
rel_injects = rel_injects,
- rel_distincts = rel_distincts},
+ rel_distincts = rel_distincts,
+ rel_sels = rel_sels},
fp_co_induct_sugar =
{co_rec = co_rec,
common_co_inducts = common_co_inducts,