--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:34:39 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:34:49 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_ctr_sugar = {ctr_transfers, case_transfers, ...},
+ ({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_sugar) =
@@ -305,7 +305,8 @@
ctr_defs = ctr_defs,
ctr_sugar = ctr_sugar,
ctr_transfers = ctr_transfers,
- case_transfers = case_transfers},
+ case_transfers = case_transfers,
+ disc_transfers = disc_transfers},
fp_bnf_sugar =
{map_thms = map_thms,
map_disc_iffs = map_disc_iffs,