# HG changeset patch
# User blanchet
# Date 1370512031 -7200
# Node ID 9606cf6770214147ae8acc57b79fc7b2934b5b10
# Parent  62f794b9e9ccd1085871643c28086ecc81149943
continuation of f461dca57c66

diff -r 62f794b9e9cc -r 9606cf677021 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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);
diff -r 62f794b9e9cc -r 9606cf677021 src/HOL/BNF/Tools/bnf_fp_util.ML
--- 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};
 
diff -r 62f794b9e9cc -r 9606cf677021 src/HOL/BNF/Tools/bnf_gfp.ML
--- 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;
diff -r 62f794b9e9cc -r 9606cf677021 src/HOL/BNF/Tools/bnf_lfp.ML
--- 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;