# HG changeset patch
# User desharna
# Date 1413293997 -7200
# Node ID eb98d1971d2a86bf6e48727d725f1a04ffaa134d
# Parent  add1a78da098367dbf56cafb4421c9552ba52dd0
add 'fp_bnf' to 'bnf_sugar'

diff -r add1a78da098 -r eb98d1971d2a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 14 15:39:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Oct 14 15:39:57 2014 +0200
@@ -54,6 +54,7 @@
      fp_res_index: int,
      fp_res: BNF_FP_Util.fp_result,
      pre_bnf: BNF_Def.bnf,
+     fp_bnf: BNF_Def.bnf,
      absT_info: BNF_Comp.absT_info,
      fp_nesting_bnfs: BNF_Def.bnf list,
      live_nesting_bnfs: BNF_Def.bnf list,
@@ -225,6 +226,7 @@
    fp_res_index: int,
    fp_res: fp_result,
    pre_bnf: bnf,
+   fp_bnf: bnf,
    absT_info: absT_info,
    fp_nesting_bnfs: bnf list,
    live_nesting_bnfs: bnf list,
@@ -275,8 +277,8 @@
    case_transfers = map (Morphism.thm phi) case_transfers,
    disc_transfers = map (Morphism.thm phi) disc_transfers};
 
-fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs,
-    live_nesting_bnfs, fp_ctr_sugar, fp_bnf_sugar,
+fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, fp_bnf, absT_info,
+    fp_nesting_bnfs, live_nesting_bnfs, fp_ctr_sugar, fp_bnf_sugar,
     fp_co_induct_sugar} : fp_sugar) =
   {T = Morphism.typ phi T,
    BT = Morphism.typ phi BT,
@@ -285,6 +287,7 @@
    fp_res = morph_fp_result phi fp_res,
    fp_res_index = fp_res_index,
    pre_bnf = morph_bnf phi pre_bnf,
+   fp_bnf = morph_bnf phi fp_bnf,
    absT_info = morph_absT_info phi absT_info,
    fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs,
    live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs,
@@ -347,6 +350,7 @@
       map_index (fn (kk, T) =>
         {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
          pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk,
+         fp_bnf = nth (#bnfs fp_res) kk,
          fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
          fp_ctr_sugar =
            {ctrXs_Tss = nth ctrXs_Tsss kk,
@@ -776,17 +780,15 @@
 
           fun mk_conjunct n k discA selAs discB selBs =
             (if k = n then [] else [HOLogic.mk_eq (discA $ ta, discB $ tb)]) @
-            (if null selAs then
-               []
+            (if null selAs then []
              else
-                [Library.foldr HOLogic.mk_imp
-                   (if n = 1 then [] else [discA $ ta, discB $ tb],
-                    Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app names_lthy Rs [])
-                      (map (rapp ta) selAs) (map (rapp tb) selBs)))]);
+               [Library.foldr HOLogic.mk_imp
+                  (if n = 1 then [] else [discA $ ta, discB $ tb],
+                   Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app names_lthy Rs [])
+                     (map (rapp ta) selAs) (map (rapp tb) selBs)))]);
 
           val goals =
-            if n = 0 then
-              []
+            if n = 0 then []
             else
               [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb,
                  (case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
diff -r add1a78da098 -r eb98d1971d2a src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 14 15:39:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Oct 14 15:39:57 2014 +0200
@@ -300,8 +300,8 @@
                 common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...},
               ...} : fp_sugar) =
           {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
-           pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
-           live_nesting_bnfs = live_nesting_bnfs,
+           pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info,
+           fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
            fp_ctr_sugar =
              {ctrXs_Tss = ctrXs_Tss,
               ctr_defs = ctr_defs,
@@ -326,7 +326,7 @@
              {co_rec = co_rec,
               common_co_inducts = common_co_inducts,
               co_inducts = co_inducts,
-              co_rec_def = co_rec_def, 
+              co_rec_def = co_rec_def,
               co_rec_thms = co_rec_thms,
               co_rec_discs = co_rec_disc_thms,
               co_rec_disc_iffs = co_rec_disc_iffs,
diff -r add1a78da098 -r eb98d1971d2a src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 14 15:39:56 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Tue Oct 14 15:39:57 2014 +0200
@@ -73,6 +73,7 @@
      fp_res =
        trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct,
      pre_bnf = ID_bnf (*wrong*),
+     fp_bnf = fp_bnf,
      absT_info = trivial_absT_info_of fpT,
      fp_nesting_bnfs = [],
      live_nesting_bnfs = [],
@@ -136,6 +137,7 @@
      fp_res =
        trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct,
      pre_bnf = ID_bnf (*wrong*),
+     fp_bnf = fp_bnf,
      absT_info = trivial_absT_info_of fpT,
      fp_nesting_bnfs = [],
      live_nesting_bnfs = [],