--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:43:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:43:28 2014 +0200
@@ -145,7 +145,7 @@
end;
val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0;
- val mapss = map #maps fp_sugars0;
+ val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0;
val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
val ctrss = map #ctrs ctr_sugars;
@@ -292,17 +292,18 @@
val phi = Proof_Context.export_morphism names_lthy no_defs_lthy;
fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
- co_rec_def maps co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
+ co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : 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, maps = maps,
+ live_nesting_bnfs = live_nesting_bnfs,
fp_ctr_sugar =
{ctrXs_Tss = ctrXs_Tss,
ctr_defs = ctr_defs,
ctr_sugar = ctr_sugar},
fp_bnf_sugar =
- {rel_injects = rel_injects,
+ {map_thms = map_thms,
+ rel_injects = rel_injects,
rel_distincts = rel_distincts},
fp_co_induct_sugar =
{co_rec = co_rec,