# HG changeset patch
# User desharna
# Date 1411735014 -7200
# Node ID 01d9908477b36ce99f63876834abe297c8108a98
# Parent  8bdcff16124de1918df5f6903566d885e0e89ddc
refactor fp_sugar with empty substructures

diff -r 8bdcff16124d -r 01d9908477b3 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:35:09 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 26 14:36:54 2014 +0200
@@ -8,6 +8,10 @@
 
 signature BNF_FP_DEF_SUGAR =
 sig
+  type fp_ctr_sugar = {}
+  type fp_bnf_sugar = {}
+  type fp_co_induct_sugar = {}
+
   type fp_sugar =
     {T: typ,
      BT: typ,
@@ -31,7 +35,10 @@
      co_rec_discs: thm list,
      co_rec_selss: thm list list,
      rel_injects: thm list,
-     rel_distincts: thm list};
+     rel_distincts: thm list,
+     fp_ctr_sugar: fp_ctr_sugar,
+     fp_bnf_sugar: fp_bnf_sugar,
+     fp_co_induct_sugar: fp_co_induct_sugar};
 
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
   val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar
@@ -151,6 +158,10 @@
 val set_inductN = "set_induct";
 val set_selN = "set_sel";
 
+type fp_ctr_sugar = {}
+type fp_bnf_sugar = {}
+type fp_co_induct_sugar = {}
+
 type fp_sugar =
   {T: typ,
    BT: typ,
@@ -174,11 +185,15 @@
    co_rec_discs: thm list,
    co_rec_selss: thm list list,
    rel_injects: thm list,
-   rel_distincts: thm list};
+   rel_distincts: thm list,
+   fp_ctr_sugar: fp_ctr_sugar,
+   fp_bnf_sugar: fp_bnf_sugar,
+   fp_co_induct_sugar: fp_co_induct_sugar};
 
 fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
     live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
-    co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts} : fp_sugar) =
+    co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts,
+    fp_ctr_sugar, fp_bnf_sugar, fp_co_induct_sugar} : fp_sugar) =
   {T = Morphism.typ phi T,
    BT = Morphism.typ phi BT,
    X = Morphism.typ phi X,
@@ -201,7 +216,10 @@
    co_rec_discs = map (Morphism.thm phi) co_rec_discs,
    co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
    rel_injects = map (Morphism.thm phi) rel_injects,
-   rel_distincts = map (Morphism.thm phi) rel_distincts};
+   rel_distincts = map (Morphism.thm phi) rel_distincts,
+   fp_ctr_sugar = fp_ctr_sugar,
+   fp_bnf_sugar = fp_bnf_sugar,
+   fp_co_induct_sugar = fp_co_induct_sugar};
 
 val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism;
 
@@ -265,7 +283,8 @@
          common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
          co_rec_thms = nth co_rec_thmss kk, co_rec_discs = nth co_rec_discss kk,
          co_rec_selss = nth co_rec_selsss kk, rel_injects = nth rel_injectss kk,
-         rel_distincts = nth rel_distinctss kk}
+         rel_distincts = nth rel_distinctss kk, fp_ctr_sugar = {}, fp_bnf_sugar = {},
+         fp_co_induct_sugar = {}}
         |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
   in
     register_fp_sugars_raw fp_sugars
diff -r 8bdcff16124d -r 01d9908477b3 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Sep 26 14:35:09 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Sep 26 14:36:54 2014 +0200
@@ -301,7 +301,8 @@
            common_co_inducts = common_co_inducts, co_inducts = co_inducts,
            co_rec_thms = co_rec_thms, co_rec_discs = co_rec_disc_thms,
            co_rec_selss = co_rec_sel_thmss, rel_injects = rel_injects,
-           rel_distincts = rel_distincts}
+           rel_distincts = rel_distincts, fp_ctr_sugar = {}, fp_bnf_sugar = {},
+           fp_co_induct_sugar = {}}
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =
diff -r 8bdcff16124d -r 01d9908477b3 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Sep 26 14:35:09 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Fri Sep 26 14:36:54 2014 +0200
@@ -88,7 +88,10 @@
      co_rec_discs = [],
      co_rec_selss = [],
      rel_injects = @{thms rel_sum_simps(1,4)},
-     rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}
+     rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
+     fp_ctr_sugar = {},
+     fp_bnf_sugar = {},
+     fp_co_induct_sugar = {}}
   end;
 
 fun fp_sugar_of_prod ctxt =
@@ -129,7 +132,10 @@
      co_rec_discs = [],
      co_rec_selss = [],
      rel_injects = @{thms rel_prod_apply},
-     rel_distincts = []}
+     rel_distincts = [],
+     fp_ctr_sugar = {},
+     fp_bnf_sugar = {},
+     fp_co_induct_sugar = {}}
   end;
 
 val _ = Theory.setup (map_local_theory (fn lthy =>