--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jun 27 10:11:44 2014 +0200
@@ -37,8 +37,8 @@
fp_res: fp_result,
pre_bnf: BNF_Def.bnf,
absT_info: BNF_Comp.absT_info,
- nested_bnfs: BNF_Def.bnf list,
- nesting_bnfs: BNF_Def.bnf list,
+ fp_nesting_bnfs: BNF_Def.bnf list,
+ live_nesting_bnfs: BNF_Def.bnf list,
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
@@ -264,8 +264,8 @@
fp_res: fp_result,
pre_bnf: bnf,
absT_info: absT_info,
- nested_bnfs: bnf list,
- nesting_bnfs: bnf list,
+ fp_nesting_bnfs: bnf list,
+ live_nesting_bnfs: bnf list,
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
@@ -280,8 +280,8 @@
rel_injects: thm list,
rel_distincts: thm list};
-fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
- nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
+fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
+ live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
{T = Morphism.typ phi T,
BT = Morphism.typ phi BT,
@@ -291,8 +291,8 @@
fp_res_index = fp_res_index,
pre_bnf = morph_bnf phi pre_bnf,
absT_info = morph_absT_info phi absT_info,
- nested_bnfs = map (morph_bnf phi) nested_bnfs,
- nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
+ live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,