# HG changeset patch
# User blanchet
# Date 1377755394 -7200
# Node ID 775b43e72d82f108ca7ad0a0f87792d4494b61d4
# Parent  f555e3659d01e9f76e6fc22897f10b3da842bf30
renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)

diff -r f555e3659d01 -r 775b43e72d82 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 29 05:42:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 29 07:49:54 2013 +0200
@@ -27,7 +27,7 @@
      xtor_rel_thms: thm list,
      xtor_co_iter_thmss: thm list list,
      xtor_co_iter_o_map_thmss: thm list list,
-     rel_co_induct_thm: thm}
+     rel_xtor_co_induct_thm: thm}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
   val eq_fp_result: fp_result * fp_result -> bool
@@ -170,7 +170,7 @@
 
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
-  val mk_rel_co_induct_thm: fp_kind -> term list -> term list -> term list -> term list ->
+  val mk_rel_xtor_co_induct_thm: fp_kind -> term list -> term list -> term list -> term list ->
     term list -> term list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
   val mk_un_fold_transfer_thms: fp_kind -> term list -> term list -> term list -> term list ->
@@ -215,11 +215,11 @@
    xtor_rel_thms: thm list,
    xtor_co_iter_thmss: thm list list,
    xtor_co_iter_o_map_thmss: thm list list,
-   rel_co_induct_thm: thm};
+   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_co_induct_thm} =
+    xtor_co_iter_thmss, xtor_co_iter_o_map_thmss, rel_xtor_co_induct_thm} =
   {Ts = map (Morphism.typ phi) Ts,
    bnfs = map (morph_bnf phi) bnfs,
    ctors = map (Morphism.term phi) ctors,
@@ -235,7 +235,7 @@
    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,
-   rel_co_induct_thm = Morphism.thm phi rel_co_induct_thm};
+   rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
 
 fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
   eq_list eq_bnf (bnfs1, bnfs2);
@@ -480,7 +480,7 @@
     Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
       right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
 
-fun mk_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
+fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
   let
     val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
     val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
diff -r f555e3659d01 -r 775b43e72d82 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 05:42:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 07:49:54 2013 +0200
@@ -2844,7 +2844,7 @@
       val Jrels = if m = 0 then map HOLogic.eq_const Ts
         else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
       val Jrel_coinduct_thm =
-        mk_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
+        mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
           Jrel_coinduct_tac lthy;
 
       val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
@@ -2894,7 +2894,7 @@
       xtor_rel_thms = dtor_Jrel_thms,
       xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
       xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_map_thms, dtor_corec_o_map_thms],
-      rel_co_induct_thm = Jrel_coinduct_thm},
+      rel_xtor_co_induct_thm = Jrel_coinduct_thm},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
diff -r f555e3659d01 -r 775b43e72d82 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 05:42:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 07:49:54 2013 +0200
@@ -1817,7 +1817,7 @@
       val Irels = if m = 0 then map HOLogic.eq_const Ts
         else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
       val Irel_induct_thm =
-        mk_rel_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
+        mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
           (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs))
           lthy;
 
@@ -1865,7 +1865,7 @@
       xtor_rel_thms = ctor_Irel_thms,
       xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
       xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_map_thms, ctor_rec_o_map_thms],
-      rel_co_induct_thm = Irel_induct_thm},
+      rel_xtor_co_induct_thm = Irel_induct_thm},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;