--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:40:02 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:40:31 2014 +0200
@@ -21,7 +21,7 @@
ctor_dtors: thm list,
ctor_injects: thm list,
dtor_injects: thm list,
- xtor_map_thms: thm list,
+ xtor_maps: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
xtor_co_rec_thms: thm list,
@@ -213,7 +213,7 @@
ctor_dtors: thm list,
ctor_injects: thm list,
dtor_injects: thm list,
- xtor_map_thms: thm list,
+ xtor_maps: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
xtor_co_rec_thms: thm list,
@@ -223,7 +223,7 @@
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_map_thms, xtor_set_thmss,
+ dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_set_thmss,
xtor_rel_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,
@@ -236,7 +236,7 @@
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
ctor_injects = map (Morphism.thm phi) ctor_injects,
dtor_injects = map (Morphism.thm phi) dtor_injects,
- xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
+ xtor_maps = map (Morphism.thm phi) xtor_maps,
xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,