--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 26 16:42:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 26 17:10:24 2015 +0100
@@ -15,6 +15,7 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
+ xtor_un_folds: term list,
xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
@@ -24,6 +25,7 @@
xtor_maps: thm list,
xtor_setss: thm list list,
xtor_rels: thm list,
+ xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_maps: thm list,
xtor_rel_co_induct: thm,
@@ -208,6 +210,7 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
+ xtor_un_folds: term list,
xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
@@ -217,20 +220,22 @@
xtor_maps: thm list,
xtor_setss: thm list list,
xtor_rels: thm list,
+ xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_maps: thm list,
xtor_rel_co_induct: thm,
dtor_set_inducts: thm list,
xtor_co_rec_transfers: thm list};
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
- dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss,
- xtor_rels, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct,
- dtor_set_inducts, xtor_co_rec_transfers} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
+ dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
+ xtor_un_fold_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct, dtor_set_inducts,
+ xtor_co_rec_transfers} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
dtors = map (Morphism.term phi) dtors,
+ xtor_un_folds = map (Morphism.term phi) xtor_un_folds,
xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
xtor_co_induct = Morphism.thm phi xtor_co_induct,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
@@ -240,6 +245,7 @@
xtor_maps = map (Morphism.thm phi) xtor_maps,
xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
xtor_rels = map (Morphism.thm phi) xtor_rels,
+ xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,