--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:41:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:41:54 2014 +0200
@@ -76,14 +76,14 @@
absT_info = trivial_absT_info_of fpT,
fp_nesting_bnfs = [],
live_nesting_bnfs = [],
- ctrXs_Tss = ctr_Tss,
- ctr_defs = @{thms Inl_def_alt Inr_def_alt},
- ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]},
maps = @{thms map_sum.simps},
common_co_inducts = @{thms sum.induct},
- fp_ctr_sugar = {},
+ 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},
fp_bnf_sugar =
{rel_injects = @{thms rel_sum_simps(1,4)},
rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}},
@@ -120,14 +120,14 @@
absT_info = trivial_absT_info_of fpT,
fp_nesting_bnfs = [],
live_nesting_bnfs = [],
- ctrXs_Tss = [ctr_Ts],
- ctr_defs = @{thms Pair_def_alt},
- ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name,
co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]},
maps = @{thms map_prod_simp},
common_co_inducts = @{thms prod.induct},
- fp_ctr_sugar = {},
+ fp_ctr_sugar =
+ {ctrXs_Tss = [ctr_Ts],
+ ctr_defs = @{thms Pair_def_alt},
+ ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name},
fp_bnf_sugar =
{rel_injects = @{thms rel_prod_apply},
rel_distincts = []},