# HG changeset patch
# User desharna
# Date 1412595552 -7200
# Node ID e2e2d775869cc35ee65d9e43521edacfd63edb6e
# Parent  8ee2d984caa84af144ef8c47059a140557d7a2ee
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'

diff -r 8ee2d984caa8 -r e2e2d775869c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:38:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Oct 06 13:39:12 2014 +0200
@@ -1936,7 +1936,7 @@
              dtors = dtors0, xtor_co_recs = xtor_co_recs0, 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_rel_co_induct, dtor_set_inducts,
-             xtor_co_rec_transfer_thms, ...},
+             xtor_co_rec_transfers, ...},
            lthy)) =
       fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
         (map dest_TFree killed_As) fp_eqs no_defs_lthy
@@ -2162,7 +2162,7 @@
         Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
           (fn {context = ctxt, prems = _} =>
              mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) rec_defs
-               xtor_co_rec_transfer_thms pre_rel_defs live_nesting_rel_eqs)
+               xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
         |> Conjunction.elim_balanced nn
         |> Proof_Context.export names_lthy lthy
         |> map Thm.close_derivation
@@ -2244,7 +2244,7 @@
         Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
           (fn {context = ctxt, prems = _} =>
              mk_corec_transfer_tac ctxt (map (certify ctxt) Ss) (map (certify ctxt) Rs)
-               type_definitions corec_defs xtor_co_rec_transfer_thms pre_rel_defs
+               type_definitions corec_defs xtor_co_rec_transfers pre_rel_defs
                live_nesting_rel_eqs (flat pgss) pss qssss gssss)
         |> Conjunction.elim_balanced (length goals)
         |> Proof_Context.export names_lthy lthy
diff -r 8ee2d984caa8 -r e2e2d775869c src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:38:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Oct 06 13:39:12 2014 +0200
@@ -478,7 +478,7 @@
         xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
         xtor_rel_co_induct = xtor_rel_co_induct,
         dtor_set_inducts = [],
-        xtor_co_rec_transfer_thms = []}
+        xtor_co_rec_transfers = []}
        |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   in
     (fp_res, lthy)
diff -r 8ee2d984caa8 -r e2e2d775869c src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:38:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Oct 06 13:39:12 2014 +0200
@@ -28,7 +28,7 @@
      xtor_co_rec_o_maps: thm list,
      xtor_rel_co_induct: thm,
      dtor_set_inducts: thm list,
-     xtor_co_rec_transfer_thms: thm list}
+     xtor_co_rec_transfers: thm list}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
 
@@ -220,12 +220,12 @@
    xtor_co_rec_o_maps: thm list,
    xtor_rel_co_induct: thm,
    dtor_set_inducts: thm list,
-   xtor_co_rec_transfer_thms: 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_map_thms, 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_transfer_thms} =
+    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,
@@ -243,7 +243,7 @@
    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,
    dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts,
-   xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
+   xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers};
 
 fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
diff -r 8ee2d984caa8 -r e2e2d775869c src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:38:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Oct 06 13:39:12 2014 +0200
@@ -2543,7 +2543,7 @@
        xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
        xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
        dtor_set_inducts = dtor_Jset_induct_thms,
-       xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
+       xtor_co_rec_transfers = dtor_corec_transfer_thms};
   in
     timer; (fp_res, lthy')
   end;
diff -r 8ee2d984caa8 -r e2e2d775869c src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:38:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Oct 06 13:39:12 2014 +0200
@@ -1829,7 +1829,7 @@
        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_maps = ctor_rec_o_Imap_thms, xtor_rel_co_induct = Irel_induct_thm,
-       dtor_set_inducts = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
+       dtor_set_inducts = [], xtor_co_rec_transfers = ctor_rec_transfer_thms};
   in
     timer; (fp_res, lthy')
   end;
diff -r 8ee2d984caa8 -r e2e2d775869c src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:38:40 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Mon Oct 06 13:39:12 2014 +0200
@@ -48,7 +48,7 @@
    xtor_co_rec_o_maps = [ctor_rec_o_map],
    xtor_rel_co_induct = xtor_rel_induct,
    dtor_set_inducts = [],
-   xtor_co_rec_transfer_thms = []};
+   xtor_co_rec_transfers = []};
 
 fun fp_sugar_of_sum ctxt =
   let