--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 11:41:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 11:47:11 2013 +0200
@@ -1080,9 +1080,8 @@
val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
xtor_un_folds = xtor_un_folds0, xtor_co_recs = xtor_co_recs0, xtor_co_induct,
- xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms,
- set_thmss = fp_set_thmss, rel_thms = fp_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms =
- xtor_co_rec_thms, ...}, lthy)) =
+ xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms,
+ xtor_set_thmss, xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms, ...}, lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
no_defs_lthy0;
@@ -1436,9 +1435,9 @@
val lthy' = lthy
|> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~
xtor_un_folds ~~ xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
- pre_set_defss ~~ pre_rel_defs ~~ fp_map_thms ~~ fp_set_thmss ~~ fp_rel_thms ~~ ns ~~ kss ~~
- mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
- raw_sel_defaultsss)
+ pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~
+ kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~
+ sel_bindingsss ~~ raw_sel_defaultsss)
|> wrap_types_etc
|> (if fp = Least_FP then derive_and_note_induct_fold_rec_thms_for_types
else derive_and_note_coinduct_unfold_corec_thms_for_types);
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jun 06 11:41:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jun 06 11:47:11 2013 +0200
@@ -22,9 +22,9 @@
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
- map_thms: thm list,
- set_thmss: thm list list,
- rel_thms: thm list,
+ xtor_map_thms: thm list,
+ xtor_set_thmss: thm list list,
+ xtor_rel_thms: thm list,
xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list}
@@ -192,15 +192,15 @@
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
- map_thms: thm list,
- set_thmss: thm list list,
- rel_thms: thm list,
+ xtor_map_thms: thm list,
+ xtor_set_thmss: thm list list,
+ xtor_rel_thms: thm list,
xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
- xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms,
- xtor_un_fold_thms, xtor_co_rec_thms} =
+ xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss,
+ xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -212,9 +212,9 @@
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
ctor_injects = map (Morphism.thm phi) ctor_injects,
- map_thms = map (Morphism.thm phi) map_thms,
- set_thmss = map (map (Morphism.thm phi)) set_thmss,
- rel_thms = map (Morphism.thm phi) rel_thms,
+ 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_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms};
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jun 06 11:41:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jun 06 11:47:11 2013 +0200
@@ -3111,8 +3111,8 @@
xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm,
xtor_strong_co_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
- map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss',
- rel_thms = dtor_Jrel_thms, xtor_un_fold_thms = ctor_dtor_unfold_thms,
+ xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
+ xtor_rel_thms = dtor_Jrel_thms, xtor_un_fold_thms = ctor_dtor_unfold_thms,
xtor_co_rec_thms = ctor_dtor_corec_thms},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 11:41:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 11:47:11 2013 +0200
@@ -1859,9 +1859,10 @@
({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds,
xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm,
xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
- ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms,
- set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms,
- xtor_un_fold_thms = ctor_fold_thms, xtor_co_rec_thms = ctor_rec_thms},
+ ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
+ xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss',
+ xtor_rel_thms = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms,
+ xtor_co_rec_thms = ctor_rec_thms},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;