src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Fri Jun 27 10:11:44 2014 +0200
@@ -237,8 +237,8 @@
         val repTs = map #repT absT_infos;
         val abs_inverses = map #abs_inverse absT_infos;
 
-        val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
-        val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
+        val fp_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss Xs;
+        val live_nesting_bnfs = nesting_bnfs lthy ctrXs_Tsss As;
 
         val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
           mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
@@ -256,15 +256,16 @@
              fp_sugar_thms) =
           if fp = Least_FP then
             derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
-              xtor_co_rec_thms nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
-              fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs lthy
+              xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
+              fp_abs_inverses fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs
+              lthy
             |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
               ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
             ||> (fn info => (SOME info, NONE))
           else
             derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
-              dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
-              fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
+              dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
+              mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
               ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
             |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
                      (sel_corec_thmsss, _)) =>
@@ -278,11 +279,11 @@
             co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
             ({rel_injects, rel_distincts, ...} : fp_sugar) =
           {T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
-           fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, nested_bnfs = nested_bnfs,
-           nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
-           ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
-           common_co_inducts = common_co_inducts, co_inducts = co_inducts,
-           co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
+           fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info,
+           fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
+           ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
+           co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts,
+           co_inducts = co_inducts, co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
            sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
           |> morph_fp_sugar phi;