--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:43:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:43:28 2014 +0200
@@ -76,13 +76,13 @@
absT_info = trivial_absT_info_of fpT,
fp_nesting_bnfs = [],
live_nesting_bnfs = [],
- maps = @{thms map_sum.simps},
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)},
+ {map_thms = @{thms map_sum.simps},
+ rel_injects = @{thms rel_sum_simps(1,4)},
rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
@@ -120,13 +120,13 @@
absT_info = trivial_absT_info_of fpT,
fp_nesting_bnfs = [],
live_nesting_bnfs = [],
- maps = @{thms map_prod_simp},
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},
+ {map_thms = @{thms map_prod_simp},
+ rel_injects = @{thms rel_prod_apply},
rel_distincts = []},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),