--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 12:48:20 2014 +0100
@@ -13,7 +13,8 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- xtor_co_iterss: term list list,
+ xtor_co_folds: term list,
+ xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
@@ -22,8 +23,10 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_co_iter_thmss: thm list list,
- xtor_co_iter_o_map_thmss: thm list list,
+ xtor_co_fold_thms: thm list,
+ xtor_co_rec_thms: thm list,
+ xtor_co_fold_o_map_thms: thm list,
+ xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm}
val morph_fp_result: morphism -> fp_result -> fp_result
@@ -193,7 +196,8 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- xtor_co_iterss: term list list,
+ xtor_co_folds: term list,
+ xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
@@ -202,18 +206,22 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_co_iter_thmss: thm list list,
- xtor_co_iter_o_map_thmss: thm list list,
+ xtor_co_fold_thms: thm list,
+ xtor_co_rec_thms: thm list,
+ xtor_co_fold_o_map_thms: thm list,
+ xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm};
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, dtor_ctors,
- ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_iter_thmss, xtor_co_iter_o_map_thmss, rel_xtor_co_induct_thm} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_folds, xtor_co_recs, xtor_co_induct,
+ dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
+ xtor_rel_thms, xtor_co_fold_thms, xtor_co_rec_thms, xtor_co_fold_o_map_thms,
+ xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
{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_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss,
+ xtor_co_folds = map (Morphism.term phi) xtor_co_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,
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
@@ -222,8 +230,10 @@
xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
- xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss,
- xtor_co_iter_o_map_thmss = map (map (Morphism.thm phi)) xtor_co_iter_o_map_thmss,
+ xtor_co_fold_thms = map (Morphism.thm phi) xtor_co_fold_thms,
+ xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
+ xtor_co_fold_o_map_thms = map (Morphism.thm phi) xtor_co_fold_o_map_thms,
+ xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
fun un_fold_of [f, _] = f;