# HG changeset patch
# User blanchet
# Date 1367521490 -7200
# Node ID d58cd7673b04c930239a1bd5a37ee642e50f668b
# Parent  4ab609682752197d72e0d8f8ac57484bc7033996
renamings

diff -r 4ab609682752 -r d58cd7673b04 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 18:48:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 21:04:50 2013 +0200
@@ -909,9 +909,10 @@
       map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
 
     val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
-           folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
-           dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
-           rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms, ...}, lthy)) =
+           un_folds = fp_folds0, co_recs = fp_recs0, co_induct = fp_induct,
+           strong_co_induct = fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects,
+           map_thms = fp_map_thms, set_thmss = fp_set_thmss, rel_thms = fp_rel_thms,
+           un_fold_thms = fp_fold_thms, co_rec_thms = fp_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;
 
diff -r 4ab609682752 -r d58cd7673b04 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 18:48:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 21:04:50 2013 +0200
@@ -13,18 +13,18 @@
      bnfs: BNF_Def.bnf list,
      ctors: term list,
      dtors: term list,
-     folds: term list,
-     recs: term list,
-     induct: thm,
-     strong_induct: thm,
+     un_folds: term list,
+     co_recs: term list,
+     co_induct: thm,
+     strong_co_induct: thm,
      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,
-     fold_thms: thm list,
-     rec_thms: thm list}
+     un_fold_thms: thm list,
+     co_rec_thms: thm list}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
   val eq_fp_result: fp_result * fp_result -> bool
@@ -183,37 +183,38 @@
    bnfs: BNF_Def.bnf list,
    ctors: term list,
    dtors: term list,
-   folds: term list,
-   recs: term list,
-   induct: thm,
-   strong_induct: thm,
+   un_folds: term list,
+   co_recs: term list,
+   co_induct: thm,
+   strong_co_induct: thm,
    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,
-   fold_thms: thm list,
-   rec_thms: thm list};
+   un_fold_thms: thm list,
+   co_rec_thms: thm list};
 
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors,
-    ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, un_folds, co_recs, co_induct, strong_co_induct,
+    dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, un_fold_thms,
+    co_rec_thms} =
   {Ts = map (Morphism.typ phi) Ts,
    bnfs = map (morph_bnf phi) bnfs,
    ctors = map (Morphism.term phi) ctors,
    dtors = map (Morphism.term phi) dtors,
-   folds = map (Morphism.term phi) folds,
-   recs = map (Morphism.term phi) recs,
-   induct = Morphism.thm phi induct,
-   strong_induct = Morphism.thm phi strong_induct,
+   un_folds = map (Morphism.term phi) un_folds,
+   co_recs = map (Morphism.term phi) co_recs,
+   co_induct = Morphism.thm phi co_induct,
+   strong_co_induct = Morphism.thm phi strong_co_induct,
    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,
-   fold_thms = map (Morphism.thm phi) fold_thms,
-   rec_thms = map (Morphism.thm phi) rec_thms};
+   un_fold_thms = map (Morphism.thm phi) un_fold_thms,
+   co_rec_thms = map (Morphism.thm phi) co_rec_thms};
 
 fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
   eq_list eq_bnf (bnfs1, bnfs2);
diff -r 4ab609682752 -r d58cd7673b04 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 18:48:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 21:04:50 2013 +0200
@@ -3027,12 +3027,12 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, folds = unfolds, recs = corecs,
-      induct = dtor_coinduct_thm, strong_induct = dtor_strong_coinduct_thm,
+    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, un_folds = unfolds, co_recs = corecs,
+      co_induct = dtor_coinduct_thm, 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, fold_thms = ctor_dtor_unfold_thms,
-      rec_thms = ctor_dtor_corec_thms},
+      rel_thms = dtor_Jrel_thms, un_fold_thms = ctor_dtor_unfold_thms,
+      co_rec_thms = ctor_dtor_corec_thms},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
diff -r 4ab609682752 -r d58cd7673b04 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 18:48:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 21:04:50 2013 +0200
@@ -1850,11 +1850,11 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, folds = folds, recs = recs,
-      induct = ctor_induct_thm, strong_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
+    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, un_folds = folds, co_recs = recs,
+      co_induct = ctor_induct_thm, 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, fold_thms = ctor_fold_thms,
-      rec_thms = ctor_rec_thms},
+      set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, un_fold_thms = ctor_fold_thms,
+      co_rec_thms = ctor_rec_thms},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;