got rid of automatically generated fold constant and theorems (to reduce overhead)

--- a/src/HOL/BNF_LFP.thy	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Mar 03 12:48:20 2014 +0100
@@ -264,4 +264,6 @@
 
 hide_fact (open) id_transfer
 
+datatype_new 'a F = F 'a
+
 end

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -21,7 +21,7 @@
 
   exception BAD_DEAD of typ * typ
 
-  val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
+  val bnf_of_typ: BNF_Def.inline_policy -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> (string * sort) list ->
     (string * sort) list -> typ -> (comp_cache * unfold_set) * Proof.context ->
     (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * Proof.context)

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -41,17 +41,17 @@
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
 
   type lfp_sugar_thms =
-    (thm list * thm * Args.src list) * (thm list list * thm list list * Args.src list)
+    (thm list * thm * Args.src list) * (thm list list * Args.src list)
 
   val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
   val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
 
   type gfp_sugar_thms =
     ((thm list * thm) list * Args.src list)
-    * (thm list list * thm list list * Args.src list)
-    * (thm list list * thm list list * Args.src list)
-    * (thm list list * thm list list * Args.src list)
-    * (thm list list list * thm list list list * Args.src list)
+    * (thm list list * Args.src list)
+    * (thm list list * Args.src list)
+    * (thm list list * Args.src list)
+    * (thm list list list * Args.src list)
 
   val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
   val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
@@ -320,11 +320,11 @@
 fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
 
 type lfp_sugar_thms =
-  (thm list * thm * Args.src list) * (thm list list * thm list list * Args.src list)
+  (thm list * thm * Args.src list) * (thm list list * Args.src list);
 
-fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) =
+fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, iter_attrs)) =
   ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
-   (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs))
+   (map (map (Morphism.thm phi)) recss, iter_attrs))
   : lfp_sugar_thms;
 
 val transfer_lfp_sugar_thms =
@@ -332,24 +332,20 @@
 
 type gfp_sugar_thms =
   ((thm list * thm) list * Args.src list)
-  * (thm list list * thm list list * Args.src list)
-  * (thm list list * thm list list * Args.src list)
-  * (thm list list * thm list list * Args.src list)
-  * (thm list list list * thm list list list * Args.src list);
+  * (thm list list * Args.src list)
+  * (thm list list * Args.src list)
+  * (thm list list * Args.src list)
+  * (thm list list list * Args.src list);
 
 fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs),
-    (unfoldss, corecss, coiter_attrs), (disc_unfoldss, disc_corecss, disc_iter_attrs),
-    (disc_unfold_iffss, disc_corec_iffss, disc_iter_iff_attrs),
-    (sel_unfoldsss, sel_corecsss, sel_iter_attrs)) =
+    (corecss, coiter_attrs), (disc_corecss, disc_iter_attrs),
+    (disc_corec_iffss, disc_iter_iff_attrs), (sel_corecsss, sel_iter_attrs)) =
   ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
     coinduct_attrs),
-   (map (map (Morphism.thm phi)) unfoldss, map (map (Morphism.thm phi)) corecss, coiter_attrs),
-   (map (map (Morphism.thm phi)) disc_unfoldss, map (map (Morphism.thm phi)) disc_corecss,
-    disc_iter_attrs),
-   (map (map (Morphism.thm phi)) disc_unfold_iffss, map (map (Morphism.thm phi)) disc_corec_iffss,
-    disc_iter_iff_attrs),
-   (map (map (map (Morphism.thm phi))) sel_unfoldsss,
-    map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms;
+   (map (map (Morphism.thm phi)) corecss, coiter_attrs),
+   (map (map (Morphism.thm phi)) disc_corecss, disc_iter_attrs),
+   (map (map (Morphism.thm phi)) disc_corec_iffss, disc_iter_iff_attrs),
+   (map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms;
 
 val transfer_gfp_sugar_thms =
   morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -386,7 +382,7 @@
       |> mk_Freessss "y" (map (map (map tl)) z_Tssss);
     val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
   in
-    ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
+    ([(h_Tss, z_Tssss, hss, zssss)], lthy)
   end;
 
 (*avoid "'a itself" arguments in coiterators*)
@@ -425,23 +421,17 @@
         (q_Tssss, f_Tsss, f_Tssss, f_repTs)
       end;
 
-    val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types un_fold_of;
     val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types co_rec_of;
 
-    val ((((Free (z, _), cs), pss), gssss), lthy) =
+    val ((((((Free (z, _), cs), pss), sssss), hssss_hd), hssss_tl), lthy) =
       lthy
       |> yield_singleton (mk_Frees "z") dummyT
       ||>> mk_Frees "a" Cs
       ||>> mk_Freess "p" p_Tss
-      ||>> mk_Freessss "g" g_Tssss;
-    val rssss = map (map (map (fn [] => []))) r_Tssss;
-
-    val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss;
-    val ((sssss, hssss_tl), lthy) =
-      lthy
-      |> mk_Freessss "q" s_Tssss
+      ||>> mk_Freessss "q" s_Tssss
+      ||>> mk_Freessss "g" h_Tssss
       ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss);
-    val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl;
+    val hssss = map2 (map2 (map2 append)) hssss_hd hssss_tl;
 
     val cpss = map2 (map o rapp) cs pss;
 
@@ -460,10 +450,9 @@
         val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss;
       in (pfss, cqfsss) end;
 
-    val unfold_args = mk_args rssss gssss g_Tsss;
     val corec_args = mk_args sssss hssss h_Tsss;
   in
-    ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
+    ((z, cs, cpss, [(corec_args, corec_types)]), lthy)
   end;
 
 fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy =
@@ -518,7 +507,7 @@
 fun define_iters iterNs iter_args_typess' mk_binding fpTs Cs reps ctor_iters lthy =
   let
     val nn = length fpTs;
-    val fpT = domain_type (snd (strip_typeN nn (fastype_of (un_fold_of ctor_iters))));
+    val fpT = domain_type (snd (strip_typeN nn (fastype_of (co_rec_of ctor_iters))));
 
     fun generate_iter pre (_, _, fss, xssss) ctor_iter =
       let val ctor_iter_absTs = map domain_type (fst (strip_typeN nn (fastype_of ctor_iter))) in
@@ -549,15 +538,15 @@
       (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy
   end;
 
-fun derive_induct_iters_thms_for_types pre_bnfs [fold_args_types, rec_args_types] ctor_induct
-    ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
-    fp_type_definitions abs_inverses ctrss ctr_defss iterss iter_defss lthy =
+fun derive_induct_iters_thms_for_types pre_bnfs [rec_args_types] ctor_induct ctor_iter_thmss
+    nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses
+    ctrss ctr_defss iterss iter_defss lthy =
   let
     val iterss' = transpose iterss;
     val iter_defss' = transpose iter_defss;
 
-    val [folds, recs] = iterss';
-    val [fold_defs, rec_defs] = iter_defss';
+    val [recs] = iterss';
+    val [rec_defs] = iter_defss';
 
     val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
 
@@ -704,15 +693,14 @@
         map2 (map2 prove) goalss tacss
       end;
 
-    val fold_thmss = mk_iter_thmss fold_args_types folds fold_defs (map un_fold_of ctor_iter_thmss);
     val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs (map co_rec_of ctor_iter_thmss);
   in
     ((induct_thms, induct_thm, [induct_case_names_attr]),
-     (fold_thmss, rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
+     (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
   end;
 
 fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
-      coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
+      coiters_args_types as [((phss, cshsss), _)])
     dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
     mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
     coiterss coiter_defss export_args lthy =
@@ -726,7 +714,7 @@
     val coiterss' = transpose coiterss;
     val coiter_defss' = transpose coiter_defss;
 
-    val [unfold_defs, corec_defs] = coiter_defss';
+    val [corec_defs] = coiter_defss';
 
     val nn = length pre_bnfs;
 
@@ -840,10 +828,10 @@
 
     fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
 
-    val fcoiterss' as [gunfolds, hcorecs] =
+    val fcoiterss' as [hcorecs] =
       map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss';
 
-    val (unfold_thmss, corec_thmss) =
+    val corec_thmss =
       let
         fun mk_goal pfss c cps fcoiter n k ctr m cfs' =
           fold_rev (fold_rev Logic.all) ([c] :: pfss)
@@ -869,50 +857,37 @@
               cqf
           end;
 
-        val crgsss' = map (map (map (build_coiter (un_fold_of fcoiterss') (K I) (K I)))) crgsss;
         val cshsss' = map (map (map (build_coiter (co_rec_of fcoiterss') (curry mk_sumT) (tack z))))
           cshsss;
 
-        val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
-        val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
+        val goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
 
-        val unfold_tacss =
-          map4 (map ooo mk_coiter_tac unfold_defs nesting_map_idents)
-            (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs abs_inverses ctr_defss;
-        val corec_tacss =
+        val tacss =
           map4 (map ooo mk_coiter_tac corec_defs nesting_map_idents)
             (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs abs_inverses ctr_defss;
 
         fun prove goal tac =
           Goal.prove_sorry lthy [] [] goal (tac o #context)
           |> Thm.close_derivation;
-
-        val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
-        val corec_thmss =
-          map2 (map2 prove) corec_goalss corec_tacss
-          |> map (map (unfold_thms lthy @{thms case_sum_if}));
       in
-        (unfold_thmss, corec_thmss)
+        map2 (map2 prove) goalss tacss
+        |> map (map (unfold_thms lthy @{thms case_sum_if}))
       end;
 
-    val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
+    val disc_corec_iff_thmss =
       let
         fun mk_goal c cps fcoiter n k disc =
           mk_Trueprop_eq (disc $ (fcoiter $ c),
             if n = 1 then @{const True}
             else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
 
-        val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss;
-        val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
+        val goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
 
         fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
 
         val case_splitss' = map (map mk_case_split') cpss;
 
-        val unfold_tacss =
-          map3 (map oo mk_disc_coiter_iff_tac) case_splitss' unfold_thmss disc_thmsss;
-        val corec_tacss =
-          map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss;
+        val tacss = map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss;
 
         fun prove goal tac =
           Goal.prove_sorry lthy [] [] goal (tac o #context)
@@ -923,12 +898,11 @@
         fun proves [_] [_] = []
           | proves goals tacs = map2 prove goals tacs;
       in
-        (map2 proves unfold_goalss unfold_tacss, map2 proves corec_goalss corec_tacss)
+        map2 proves goalss tacss
       end;
 
     fun mk_disc_coiter_thms coiters discIs = map (op RS) (coiters ~~ discIs);
 
-    val disc_unfold_thmss = map2 mk_disc_coiter_thms unfold_thmss discIss;
     val disc_corec_thmss = map2 mk_disc_coiter_thms corec_thmss discIss;
 
     fun mk_sel_coiter_thm coiter_thm sel sel_thm =
@@ -946,7 +920,6 @@
     fun mk_sel_coiter_thms coiter_thmss =
       map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss;
 
-    val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss;
     val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss;
 
     val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
@@ -959,10 +932,10 @@
       coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   in
     ((coinduct_thms_pairs, coinduct_case_attrs),
-     (unfold_thmss, corec_thmss, code_nitpicksimp_attrs),
-     (disc_unfold_thmss, disc_corec_thmss, []),
-     (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
-     (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
+     (corec_thmss, code_nitpicksimp_attrs),
+     (disc_corec_thmss, []),
+     (disc_corec_iff_thmss, simp_attrs),
+     (sel_corec_thmsss, simp_attrs))
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
@@ -1368,11 +1341,9 @@
         (wrap_ctrs
          #> derive_maps_sets_rels
          ##>>
-           (if fp = Least_FP then
-             define_iters [foldN, recN] (the iters_args_types) mk_binding fpTs Cs reps xtor_co_iters
-           else
-             define_coiters [unfoldN, corecN] (the coiters_args_types) mk_binding fpTs Cs abss
-               xtor_co_iters)
+           (if fp = Least_FP then define_iters [recN] (the iters_args_types) mk_binding fpTs Cs reps
+           else define_coiters [corecN] (the coiters_args_types) mk_binding fpTs Cs abss)
+             [co_rec_of xtor_co_iters]
          #> massage_res, lthy')
       end;
 
@@ -1381,16 +1352,15 @@
       |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list)
         o split_list;
 
-    fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) un_folds co_recs
-        mapsx rel_injects rel_distincts setss =
-      injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects @ rel_distincts
-      @ flat setss;
+    fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs mapsx rel_injects
+        rel_distincts setss =
+      injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
 
     fun derive_note_induct_iters_thms_for_types
         ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
           (iterss, iter_defss)), lthy) =
       let
-        val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, iter_attrs)) =
+        val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, iter_attrs)) =
           derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
             xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
             type_definitions abs_inverses ctrss ctr_defss iterss iter_defss lthy;
@@ -1398,26 +1368,24 @@
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
 
         val simp_thmss =
-          map7 mk_simp_thms ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss;
+          map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss;
 
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
           |> massage_simple_notes fp_common_name;
 
         val notes =
-          [(foldN, fold_thmss, K iter_attrs),
-           (inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
+          [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
            (recN, rec_thmss, K iter_attrs),
            (simpsN, simp_thmss, K [])]
           |> massage_multi_notes;
       in
         lthy
-        |> Spec_Rules.add Spec_Rules.Equational (map un_fold_of iterss, flat fold_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
           ctrXs_Tsss ctr_defss ctr_sugars iterss mapss [induct_thm] (map single induct_thms)
-          (transpose [fold_thmss, rec_thmss]) (replicate nn []) (replicate nn [])
+          (map single rec_thmss) (replicate nn []) (replicate nn [])
       end;
 
     fun derive_note_coinduct_coiters_thms_for_types
@@ -1426,16 +1394,15 @@
       let
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
               coinduct_attrs),
-             (unfold_thmss, corec_thmss, coiter_attrs),
-             (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
-             (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
-             (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
+             (corec_thmss, coiter_attrs),
+             (disc_corec_thmss, disc_coiter_attrs),
+             (disc_corec_iff_thmss, disc_coiter_iff_attrs),
+             (sel_corec_thmsss, sel_coiter_attrs)) =
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
             abs_inverses abs_inverses I ctr_defss ctr_sugars coiterss coiter_defss
             (Proof_Context.export lthy' no_defs_lthy) lthy;
 
-        val sel_unfold_thmss = map flat sel_unfold_thmsss;
         val sel_corec_thmss = map flat sel_corec_thmsss;
 
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
@@ -1443,8 +1410,7 @@
         val flat_coiter_thms = append oo append;
 
         val simp_thmss =
-          map7 mk_simp_thms ctr_sugars
-            (map3 flat_coiter_thms disc_unfold_thmss disc_unfold_iff_thmss sel_unfold_thmss)
+          map6 mk_simp_thms ctr_sugars
             (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
             mapss rel_injects rel_distincts setss;
 
@@ -1462,13 +1428,9 @@
            (corecN, corec_thmss, K coiter_attrs),
            (disc_corecN, disc_corec_thmss, K disc_coiter_attrs),
            (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs),
-           (disc_unfoldN, disc_unfold_thmss, K disc_coiter_attrs),
-           (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_coiter_iff_attrs),
            (sel_corecN, sel_corec_thmss, K sel_coiter_attrs),
-           (sel_unfoldN, sel_unfold_thmss, K sel_coiter_attrs),
            (simpsN, simp_thmss, K []),
-           (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
-           (unfoldN, unfold_thmss, K coiter_attrs)]
+           (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
           |> massage_multi_notes;
 
         (* TODO: code theorems *)
@@ -1477,14 +1439,12 @@
             [flat sel_thmss, flat ctr_thmss]
       in
         lthy
-        |> add_spec_rules un_fold_of sel_unfold_thmss unfold_thmss
         |> add_spec_rules co_rec_of sel_corec_thmss corec_thmss
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
           ctrXs_Tsss ctr_defss ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
-          (transpose [coinduct_thms, strong_coinduct_thms])
-          (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
-          (transpose [sel_unfold_thmsss, sel_corec_thmsss])
+          (transpose [coinduct_thms, strong_coinduct_thms]) (map single corec_thmss)
+          (map single disc_corec_thmss) (map single sel_corec_thmsss)
       end;
 
     val lthy'' = lthy'

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -248,53 +248,47 @@
         val ((co_iterss, co_iter_defss), lthy) =
           fold_map2 (fn b =>
             if fp = Least_FP then
-              define_iters [foldN, recN] (the iters_args_types) (mk_binding b) fpTs Cs reps
+              define_iters [recN] (the iters_args_types) (mk_binding b) fpTs Cs reps
             else
-              define_coiters [unfoldN, corecN] (the coiters_args_types) (mk_binding b) fpTs Cs abss)
-            fp_bs xtor_co_iterss lthy
+              define_coiters [corecN] (the coiters_args_types) (mk_binding b) fpTs Cs abss)
+            fp_bs (map (single o co_rec_of) xtor_co_iterss) lthy
           |>> split_list;
 
-        val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
-              disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
+        val ((common_co_inducts, co_inductss, co_rec_thmss, disc_corec_thmss, sel_corec_thmsss),
+             fp_sugar_thms) =
           if fp = Least_FP then
             derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
               xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
               fp_type_definitions abs_inverses ctrss ctr_defss co_iterss co_iter_defss lthy
-            |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
-              ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [],
-               replicate nn [], replicate nn [], replicate nn []))
+            |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
+              ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
             ||> (fn info => (SOME info, NONE))
           else
             derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
               dtor_injects dtor_ctors xtor_co_iter_thmss 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_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
-            |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
-                    (disc_unfold_thmss, disc_corec_thmss, _), _,
-                    (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
-              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss,
-               corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss,
-               sel_corec_thmsss))
+            |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
+                     (sel_corec_thmsss, _)) =>
+              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
+               disc_corec_thmss, sel_corec_thmsss))
             ||> (fn info => (NONE, SOME info));
 
         val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
         fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_iters maps
-            co_inducts un_fold_thms co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss
-            sel_corec_thmss =
+            co_inducts co_rec_thms disc_corec_thms sel_corec_thmss =
           {T = T, 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_iters = co_iters,
            maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts,
-           co_iter_thmss = [un_fold_thms, co_rec_thms],
-           disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
-           sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]}
+           co_iter_thmss = [co_rec_thms], disc_co_iterss = [disc_corec_thms],
+           sel_co_itersss = [sel_corec_thmss]}
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =
-          map17 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
-            co_iterss mapss (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss
-            disc_corec_thmss sel_unfold_thmsss sel_corec_thmsss;
+          map14 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
+            co_iterss mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss;
 
         val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
       in

--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -34,7 +34,6 @@
   val permute_args: int -> term -> term
 
   val mk_partial_compN: int -> typ -> term -> term
-  val mk_partial_comp: typ -> typ -> term -> term
   val mk_compN: int -> typ list -> term * term -> term
   val mk_comp: typ list -> term * term -> term
 
@@ -93,13 +92,10 @@
 fun permute_args n t =
   list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n);
 
-fun mk_partial_comp gT fT g = fst (Term.dest_comb (HOLogic.mk_comp (g, Free (Name.uu, fT))));
+fun mk_partial_comp fT g = fst (Term.dest_comb (HOLogic.mk_comp (g, Free (Name.uu, fT))));
 
 fun mk_partial_compN 0 _ g = g
-  | mk_partial_compN n fT g =
-    let val g' = mk_partial_compN (n - 1) (range_type fT) g in
-      mk_partial_comp (fastype_of g') fT g'
-    end;
+  | mk_partial_compN n fT g = mk_partial_comp fT (mk_partial_compN (n - 1) (range_type fT) g);
 
 fun mk_compN n bound_Ts (g, f) =
   let val typof = curry fastype_of1 bound_Ts in

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -62,8 +62,6 @@
   val ctor_relN: string
   val ctor_set_inclN: string
   val ctor_set_set_inclN: string
-  val disc_unfoldN: string
-  val disc_unfold_iffN: string
   val disc_corecN: string
   val disc_corec_iffN: string
   val dtorN: string
@@ -87,7 +85,6 @@
   val dtor_unfold_transferN: string
   val dtor_unfold_uniqueN: string
   val exhaustN: string
-  val foldN: string
   val hsetN: string
   val hset_recN: string
   val inductN: string
@@ -108,7 +105,6 @@
   val sel_corecN: string
   val set_inclN: string
   val set_set_inclN: string
-  val sel_unfoldN: string
   val setN: string
   val simpsN: string
   val strTN: string
@@ -116,7 +112,6 @@
   val strong_coinductN: string
   val sum_bdN: string
   val sum_bdTN: string
-  val unfoldN: string
   val uniqueN: string
 
   (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *)
@@ -232,7 +227,9 @@
    rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
 
 fun un_fold_of [f, _] = f;
-fun co_rec_of [_, r] = r;
+
+fun co_rec_of [r] = r
+  | co_rec_of [_, r] = r;
 
 fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
@@ -325,10 +322,8 @@
 
 val caseN = "case"
 val discN = "disc"
-val disc_unfoldN = discN ^ "_" ^ unfoldN
 val disc_corecN = discN ^ "_" ^ corecN
 val iffN = "_iff"
-val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
 val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
 val distinctN = "distinct"
 val rel_distinctN = relN ^ "_" ^ distinctN
@@ -337,7 +332,6 @@
 val rel_coinductN = relN ^ "_" ^ coinductN
 val rel_inductN = relN ^ "_" ^ inductN
 val selN = "sel"
-val sel_unfoldN = selN ^ "_" ^ unfoldN
 val sel_corecN = selN ^ "_" ^ corecN
 
 fun co_prefix fp = (if fp = Greatest_FP then "co" else "");

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -163,7 +163,7 @@
     val all_notes =
       (case lfp_sugar_thms of
         NONE => []
-      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) =>
+      | SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) =>
         let
           val common_notes =
             (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -172,8 +172,7 @@
               ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
 
           val notes =
-            [(foldN, fold_thmss, []),
-             (inductN, map single induct_thms, induct_attrs),
+            [(inductN, map single induct_thms, induct_attrs),
              (recN, rec_thmss, code_nitpicksimp_simp_attrs)]
             |> filter_out (null o #2)
             |> maps (fn (thmN, thmss, attrs) =>

--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -35,19 +35,6 @@
       'o) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
-  val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
-      'o -> 'p) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
-  val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
-      'o -> 'p -> 'q) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
-  val map17: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
-      'o -> 'p -> 'q -> 'r) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list ->
-    'q list -> 'r list
   val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
   val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
@@ -216,29 +203,6 @@
       map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
   | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
-fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ::
-      map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
-  | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s)
-      (x16::x16s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 ::
-      map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s
-  | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map17 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map17 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s)
-      (x16::x16s) (x17::x17s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 ::
-      map17 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s x17s
-  | map17 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
 fun fold_map4 _ [] [] [] [] acc = ([], acc)
   | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
     let