--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:34:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:34:24 2014 +0200
@@ -79,7 +79,8 @@
fp_ctr_sugar =
{ctrXs_Tss = ctr_Tss,
ctr_defs = @{thms Inl_def_alt Inr_def_alt},
- ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
+ ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
+ ctr_transfers = []},
fp_bnf_sugar =
{map_thms = @{thms map_sum.simps},
map_disc_iffs = [],
@@ -132,7 +133,8 @@
fp_ctr_sugar =
{ctrXs_Tss = [ctr_Ts],
ctr_defs = @{thms Pair_def_alt},
- ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
+ ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
+ ctr_transfers = []},
fp_bnf_sugar =
{map_thms = @{thms map_prod_simp},
map_disc_iffs = [],