--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:36:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Oct 06 13:37:38 2014 +0200
@@ -388,7 +388,7 @@
val co_recs = map (Morphism.term phi) raw_co_recs;
- val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms
+ val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_maps
|> maps (fn thm => [thm, thm RS rewrite_comp_comp]);
val xtor_co_rec_thms =
@@ -475,7 +475,7 @@
xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
xtor_co_rec_thms = xtor_co_rec_thms,
- xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
+ xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
dtor_set_induct_thms = [],
xtor_co_rec_transfer_thms = []}
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:36:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Oct 06 13:37:38 2014 +0200
@@ -25,7 +25,7 @@
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
xtor_co_rec_thms: thm list,
- xtor_co_rec_o_map_thms: thm list,
+ xtor_co_rec_o_maps: thm list,
rel_xtor_co_induct_thm: thm,
dtor_set_induct_thms: thm list,
xtor_co_rec_transfer_thms: thm list}
@@ -217,14 +217,14 @@
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
xtor_co_rec_thms: thm list,
- xtor_co_rec_o_map_thms: thm list,
+ xtor_co_rec_o_maps: thm list,
rel_xtor_co_induct_thm: thm,
dtor_set_induct_thms: thm list,
xtor_co_rec_transfer_thms: 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,
- xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
+ xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, rel_xtor_co_induct_thm,
dtor_set_induct_thms, xtor_co_rec_transfer_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
@@ -240,7 +240,7 @@
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,
- xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
+ xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:36:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Oct 06 13:37:38 2014 +0200
@@ -2541,7 +2541,7 @@
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
- xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
+ xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
dtor_set_induct_thms = dtor_Jset_induct_thms,
xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
in
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:36:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Oct 06 13:37:38 2014 +0200
@@ -1828,7 +1828,7 @@
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
- xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
+ xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
in
timer; (fp_res, lthy')
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:36:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:37:38 2014 +0200
@@ -45,7 +45,7 @@
xtor_set_thmss = [xtor_sets],
xtor_rel_thms = [xtor_rel],
xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
- xtor_co_rec_o_map_thms = [ctor_rec_o_map],
+ xtor_co_rec_o_maps = [ctor_rec_o_map],
rel_xtor_co_induct_thm = xtor_rel_induct,
dtor_set_induct_thms = [],
xtor_co_rec_transfer_thms = []};
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Oct 06 13:36:48 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Oct 06 13:37:38 2014 +0200
@@ -82,7 +82,7 @@
IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
- fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
+ fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_maps = ctor_rec_o_maps, ...}, fp_nesting_bnfs,
live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
let
val data = Data.get (Context.Proof lthy0);