--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:33:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:34:04 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, rel_cases, set_thms, set_sels, ...}, ...} : fp_sugar) =
+ rel_intros, rel_cases, set_thms, set_sels, set_intros, ...}, ...} : 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,
@@ -312,7 +312,8 @@
rel_intros = rel_intros,
rel_cases = rel_cases,
set_thms = set_thms,
- set_sels = set_sels},
+ set_sels = set_sels,
+ set_intros = set_intros},
fp_co_induct_sugar =
{co_rec = co_rec,
common_co_inducts = common_co_inducts,