merged;
authorwenzelm
Mon, 03 Mar 2014 15:14:00 +0100
changeset 55886 b11b358fec57
parent 55875 6478b12b7297 (diff)
parent 55885 c871a2e751ec (current diff)
child 55887 25bd4745ee38
merged;
--- a/NEWS	Mon Mar 03 13:54:47 2014 +0100
+++ b/NEWS	Mon Mar 03 15:14:00 2014 +0100
@@ -112,8 +112,7 @@
 
 * Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
   The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
-  "primrec_new", "primcorec", and "primcorecursive" command are now part of
-  "Main".
+  "primcorec", and "primcorecursive" commands are now part of "Main".
   Theory renamings:
     FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
     Library/Wfrec.thy ~> Wfrec.thy
@@ -146,18 +145,26 @@
   Discontinued theories:
     BNF/BNF.thy
     BNF/Equiv_Relations_More.thy
-  Renamed commands:
-    datatype_new_compat ~> datatype_compat
-    primrec_new ~> primrec
-    wrap_free_constructors ~> free_constructors
   INCOMPATIBILITY.
 
+* New datatype package:
+  * "primcorec" is fully implemented.
+  * Renamed commands:
+      datatype_new_compat ~> datatype_compat
+      primrec_new ~> primrec
+      wrap_free_constructors ~> free_constructors
+    INCOMPATIBILITY.
+  * The generated constants "xxx_case" and "xxx_rec" have been renamed
+    "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
+    INCOMPATIBILITY.
+  * The constant "xxx_(un)fold" and related theorems are no longer generated.
+    Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec".
+    INCOMPATIBILITY.
+
 * Old datatype package:
   * The generated theorems "xxx.cases" and "xxx.recs" have been renamed
     "xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
     INCOMPATIBILITY.
-
-* Old and new (co)datatype packages:
   * The generated constants "xxx_case" and "xxx_rec" have been renamed
     "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
     INCOMPATIBILITY.
@@ -169,10 +176,12 @@
     Option.set ~> set_option
     Option.map ~> map_option
     option_rel ~> rel_option
+    option_rec ~> case_option
   Renamed theorems:
     set_def ~> set_rec[abs_def]
     map_def ~> map_rec[abs_def]
     Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
+    option.recs ~> option.case
     list_all2_def ~> list_all2_iff
     set.simps ~> set_simps (or the slightly different "list.set")
     map.simps ~> list.map
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -619,9 +619,9 @@
 \begin{itemize}
 \setlength{\itemsep}{0pt}
 
-\item The old-style, nested-as-mutual induction rule, iterator theorems, and
-recursor theorems are generated under their usual names but with ``@{text
-"compat_"}'' prefixed (e.g., @{text compat_tree.induct}).
+\item The old-style, nested-as-mutual induction rule and recursor theorems are
+generated under their usual names but with ``@{text "compat_"}'' prefixed
+(e.g., @{text compat_tree.induct}).
 
 \item All types through which recursion takes place must be new-style datatypes
 or the function type. In principle, it should be possible to support old-style
@@ -665,8 +665,6 @@
   @{text t.map_t} \\
 Relator: &
   @{text t.rel_t} \\
-Iterator: &
-   @{text t.fold_t} \\
 Recursor: &
   @{text t.rec_t}
 \end{tabular}
@@ -934,10 +932,6 @@
 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
 prove $m$ properties simultaneously.
 
-\item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\
-@{thm list.fold(1)[no_vars]} \\
-@{thm list.fold(2)[no_vars]}
-
 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.rec(1)[no_vars]} \\
 @{thm list.rec(2)[no_vars]}
@@ -951,7 +945,7 @@
 \begin{indentblock}
 \begin{description}
 
-\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject}] ~ \\
 @{text t.rel_distinct} @{text t.set}
 
 \end{description}
@@ -1402,7 +1396,7 @@
 %  * induct
 %    * mutualized
 %    * without some needless induction hypotheses if not used
-%  * fold, rec
+%  * rec
 %    * mutualized
 *}
 *)
@@ -1627,13 +1621,11 @@
 with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
 \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
-iterator and the recursor are replaced by dual concepts:
+recursor is replaced by a dual concept:
 
 \medskip
 
 \begin{tabular}{@ {}ll@ {}}
-Coiterator: &
-  @{text unfold_t} \\
 Corecursor: &
   @{text corec_t}
 \end{tabular}
@@ -1696,34 +1688,18 @@
 Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
 used to prove $m$ properties simultaneously.
 
-\item[@{text "t."}\hthm{unfold}\rm:] ~ \\
-@{thm llist.unfold(1)[no_vars]} \\
-@{thm llist.unfold(2)[no_vars]}
-
 \item[@{text "t."}\hthm{corec}\rm:] ~ \\
 @{thm llist.corec(1)[no_vars]} \\
 @{thm llist.corec(2)[no_vars]}
 
-\item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\
-@{thm llist.disc_unfold(1)[no_vars]} \\
-@{thm llist.disc_unfold(2)[no_vars]}
-
 \item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
 @{thm llist.disc_corec(1)[no_vars]} \\
 @{thm llist.disc_corec(2)[no_vars]}
 
-\item[@{text "t."}\hthm{disc\_unfold\_iff} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.disc_unfold_iff(1)[no_vars]} \\
-@{thm llist.disc_unfold_iff(2)[no_vars]}
-
 \item[@{text "t."}\hthm{disc\_corec\_iff} @{text "[simp]"}\rm:] ~ \\
 @{thm llist.disc_corec_iff(1)[no_vars]} \\
 @{thm llist.disc_corec_iff(2)[no_vars]}
 
-\item[@{text "t."}\hthm{sel\_unfold} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.sel_unfold(1)[no_vars]} \\
-@{thm llist.sel_unfold(2)[no_vars]}
-
 \item[@{text "t."}\hthm{sel\_corec} @{text "[simp]"}\rm:] ~ \\
 @{thm llist.sel_corec(1)[no_vars]} \\
 @{thm llist.sel_corec(2)[no_vars]}
@@ -1738,8 +1714,7 @@
 \begin{description}
 
 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec} @{text t.disc_corec_iff}] ~ \\
-@{text t.sel_corec} @{text t.disc_unfold} @{text t.disc_unfold_iff} @{text t.sel_unfold} @{text t.map} \\
-@{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
+@{text t.sel_corec} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
 
 \end{description}
 \end{indentblock}
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -199,7 +199,7 @@
   "Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
 unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
 
-lemma Cinfinite_csum_strong:
+lemma Cinfinite_csum_weak:
   "\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
 by (erule Cinfinite_csum1)
 
@@ -335,6 +335,9 @@
 lemma cprod_mono2: "p2 \<le>o r2 \<Longrightarrow> q *c p2 \<le>o q *c r2"
 by (simp only: cprod_def ordLeq_Times_mono2)
 
+lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
+by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
+
 lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
 unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
 
@@ -347,6 +350,15 @@
 lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
 by (blast intro: cinfinite_cprod2 Card_order_cprod)
 
+lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono)
+
+lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono1)
+
+lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono2)
+
 lemma cprod_com: "p1 *c p2 =o p2 *c p1"
 by (simp only: cprod_def card_of_Times_commute)
 
@@ -514,6 +526,9 @@
 unfolding cinfinite_def cprod_def
 by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+
 
+lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
+using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
+
 lemma cexp_cprod_ordLeq:
   assumes r1: "Card_order r1" and r2: "Cinfinite r2"
   and r3: "Cnotzero r3" "r3 \<le>o r2"
--- a/src/HOL/BNF_Comp.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -128,7 +128,26 @@
 
 end
 
+definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp = (\<lambda>x. x)"
+
+lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
+  unfolding id_bnf_comp_def by unfold_locales auto
+
+lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
+apply (erule ordIso_transitive)
+apply (frule csum_absorb2')
+apply (erule ordLeq_refl)
+by simp
+
+lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
+apply (erule ordIso_transitive)
+apply (rule cprod_infinite)
+by simp
+
 ML_file "Tools/BNF/bnf_comp_tactics.ML"
 ML_file "Tools/BNF/bnf_comp.ML"
 
+hide_const (open) id_bnf_comp
+hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
+
 end
--- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -20,7 +20,7 @@
 
 definition "Node n as \<equiv> NNode n (the_inv fset as)"
 definition "cont \<equiv> fset o ccont"
-definition "unfold rt ct \<equiv> unfold_dtree rt (the_inv fset o ct)"
+definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (sum_map id Inr) o ct)"
 definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
 
 lemma finite_cont[simp]: "finite (cont tr)"
@@ -75,18 +75,16 @@
 lemma unfold:
 "root (unfold rt ct b) = rt b"
 "finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
-using dtree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def
-apply - apply metis
+using dtree.sel_corec[of rt "the_inv fset o image (sum_map id Inr) o ct" b] unfolding unfold_def
+apply blast
 unfolding cont_def comp_def
-by simp
+by (simp add: case_sum_o_inj sum_map.compositionality image_image)
 
 lemma corec:
 "root (corec rt ct b) = rt b"
 "finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
 using dtree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
-apply -
-apply simp
 unfolding cont_def comp_def id_def
-by simp
+by simp_all
 
 end
--- a/src/HOL/BNF_Examples/Misc_Primcorec.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -88,26 +88,26 @@
   id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
   id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
 where
-  "id_tree t = (case t of BRTree a ts ts' => BRTree a (id_trees1 ts) (id_trees2 ts'))" |
+  "id_tree t = (case t of BRTree a ts ts' \<Rightarrow> BRTree a (id_trees1 ts) (id_trees2 ts'))" |
   "id_trees1 ts = (case ts of
-       MyNil => MyNil
-     | MyCons t ts => MyCons (id_tree t) (id_trees1 ts))" |
+       MyNil \<Rightarrow> MyNil
+     | MyCons t ts \<Rightarrow> MyCons (id_tree t) (id_trees1 ts))" |
   "id_trees2 ts = (case ts of
-       MyNil => MyNil
-     | MyCons t ts => MyCons (id_tree t) (id_trees2 ts))"
+       MyNil \<Rightarrow> MyNil
+     | MyCons t ts \<Rightarrow> MyCons (id_tree t) (id_trees2 ts))"
 
 primcorec
   trunc_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
   trunc_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
   trunc_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
 where
-  "trunc_tree t = (case t of BRTree a ts ts' => BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" |
+  "trunc_tree t = (case t of BRTree a ts ts' \<Rightarrow> BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" |
   "trunc_trees1 ts = (case ts of
-       MyNil => MyNil
-     | MyCons t _ => MyCons (trunc_tree t) MyNil)" |
+       MyNil \<Rightarrow> MyNil
+     | MyCons t _ \<Rightarrow> MyCons (trunc_tree t) MyNil)" |
   "trunc_trees2 ts = (case ts of
-       MyNil => MyNil
-     | MyCons t ts => MyCons (trunc_tree t) MyNil)"
+       MyNil \<Rightarrow> MyNil
+     | MyCons t ts \<Rightarrow> MyCons (trunc_tree t) MyNil)"
 
 primcorec
   freeze_exp :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) exp \<Rightarrow> ('a, 'b) exp" and
--- a/src/HOL/BNF_Examples/Stream.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -33,16 +33,16 @@
   assume "a \<in> set1_pre_stream (dtor_stream s)"
   then have "a = shd s"
     by (cases "dtor_stream s")
-      (auto simp: shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
-        Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits)
+      (auto simp: BNF_Comp.id_bnf_comp_def shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
+        split: stream.splits)
   with Base show "P a s" by simp
 next
   fix a :: 'a and s' :: "'a stream"  and s :: "'a stream"
   assume "s' \<in> set2_pre_stream (dtor_stream s)" and prems: "a \<in> sset s'" "P a s'"
   then have "s' = stl s"
     by (cases "dtor_stream s")
-      (auto simp: stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
-        Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits)
+      (auto simp: BNF_Comp.id_bnf_comp_def stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
+        split: stream.splits)
   with Step prems show "P a s" by simp
 qed
 
--- a/src/HOL/BNF_FP_Base.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -177,6 +177,9 @@
     type_definition.Abs_inverse[OF assms(1) UNIV_I]
     type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
 
+lemma vimage2p_id: "vimage2p id id R = R"
+  unfolding vimage2p_def by auto
+
 lemma vimage2p_comp: "vimage2p (f1 o f2) (g1 o g2) = vimage2p f2 g2 o vimage2p f1 g1"
   unfolding fun_eq_iff vimage2p_def o_apply by simp
 
--- a/src/HOL/BNF_LFP.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -251,10 +251,10 @@
   unfolding vimage2p_def by auto
 
 lemma id_transfer: "fun_rel A A id id"
-unfolding fun_rel_def by simp
+  unfolding fun_rel_def by simp
 
 lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
-  by simp
+  by (rule ssubst)
 
 ML_file "Tools/BNF/bnf_lfp_util.ML"
 ML_file "Tools/BNF/bnf_lfp_tactics.ML"
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -66,18 +66,10 @@
   unfolding cprod_def cone_def Field_card_of
   by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton])
 
-lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
-by (simp only: cprod_def ordIso_Times_cong2)
 
 lemma ordLeq_cprod1: "\<lbrakk>Card_order p1; Cnotzero p2\<rbrakk> \<Longrightarrow> p1 \<le>o p1 *c p2"
 unfolding cprod_def by (metis Card_order_Times1 czeroI)
 
-lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
-using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
-
-lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
-  by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
-
 
 subsection {* Exponentiation *}
 
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -585,20 +585,6 @@
 nitpick [expect = genuine]
 oops
 
-lemma "rec_option n s None = n"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "rec_option n s (Some x) = s x"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "P (rec_option n s x)"
-nitpick [expect = genuine]
-oops
-
 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
 nitpick [expect = genuine]
 oops
--- a/src/HOL/Option.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Option.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -28,7 +28,6 @@
 setup {* Sign.mandatory_path "option" *}
 
 lemmas inducts = option.induct
-lemmas recs = option.rec
 lemmas cases = option.case
 
 setup {* Sign.parent_path *}
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -6,6 +6,8 @@
 Composition of bounded natural functors.
 *)
 
+val inline_ref = Unsynchronized.ref true;
+
 signature BNF_COMP =
 sig
   val ID_bnf: BNF_Def.bnf
@@ -19,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)
@@ -95,6 +97,10 @@
     val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
   in Envir.expand_term get end;
 
+fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
+  | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
+  | is_sum_prod_natLeq t = t aconv @{term natLeq};
+
 fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
   let
     val olive = live_of_bnf outer;
@@ -170,6 +176,20 @@
     (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
     val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
 
+    val (bd', bd_ordIso_natLeq_thm_opt) =
+      if is_sum_prod_natLeq bd then
+        let
+          val bd' = @{term natLeq};
+          val bd_bd' = HOLogic.mk_prod (bd, bd');
+          val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
+          val goal = HOLogic.mk_Trueprop (HOLogic.mk_mem (bd_bd', ordIso));
+        in
+          (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
+            |> Thm.close_derivation))
+        end
+      else
+        (bd, NONE);
+
     fun map_id0_tac _ =
       mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
         (map map_id0_of_bnf inners);
@@ -220,7 +240,7 @@
             map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
         in
           map2 (fn set_alt => fn single_set_bds => fn ctxt =>
-            mk_comp_set_bd_tac ctxt set_alt single_set_bds)
+            mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
           set_alt_thms single_set_bd_thmss
         end;
 
@@ -278,7 +298,7 @@
 
     val (bnf', lthy') =
       bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
-        Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy;
+        Binding.empty [] ((((((b, CCA), mapx), sets), bd'), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -610,18 +630,44 @@
   let val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
   in Term.typ_subst_TVars rho absT end;
 
-fun mk_repT (t as Type (C, Ts)) repT (u as Type (C', Us)) =
-    if C = C' andalso length Ts = length Us then Term.typ_subst_atomic (Ts ~~ Us) repT
-    else raise Term.TYPE ("mk_repT", [t, repT, u], [])
-  | mk_repT t repT u =  raise Term.TYPE ("mk_repT", [t, repT, u], []);
+fun mk_repT absT repT absU =
+  if absT = repT then absU
+  else
+    (case (absT, absU) of
+      (Type (C, Ts), Type (C', Us)) =>
+        if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT
+        else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
+    | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
 
-fun mk_abs_or_rep getT (Type (_, Us)) abs =
-  let val Ts = snd (dest_Type (getT (fastype_of abs)))
-  in Term.subst_atomic_types (Ts ~~ Us) abs end;
+fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf_comp}, _)) =
+    Const (@{const_name id_bnf_comp}, absU --> absU)
+  | mk_abs_or_rep getT (Type (_, Us)) abs =
+    let val Ts = snd (dest_Type (getT (fastype_of abs)))
+    in Term.subst_atomic_types (Ts ~~ Us) abs end;
 
 val mk_abs = mk_abs_or_rep range_type;
 val mk_rep = mk_abs_or_rep domain_type;
 
+val smart_max_inline_type_size = 5; (*FUDGE*)
+
+fun maybe_typedef (b, As, mx) set opt_morphs tac =
+  let
+    val repT = HOLogic.dest_setT (fastype_of set);
+    val inline = Term.size_of_typ repT <= smart_max_inline_type_size;
+  in
+    if inline then
+      pair (repT,
+        (@{const_name id_bnf_comp}, @{const_name id_bnf_comp},
+         @{thm type_definition_id_bnf_comp_UNIV},
+         @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_comp_UNIV]},
+         @{thm type_definition.Abs_inject[OF type_definition_id_bnf_comp_UNIV]}))
+    else
+      typedef (b, As, mx) set opt_morphs tac
+      #>> (fn (T_name, ({Rep_name, Abs_name, ...},
+          {type_definition, Abs_inverse, Abs_inject, ...}) : Typedef.info) =>
+        (Type (T_name, map TFree As), (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject)))
+  end;
+
 fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
   let
     val live = live_of_bnf bnf;
@@ -652,25 +698,23 @@
     fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
 
     val repTA = mk_T_of_bnf Ds As bnf;
-    val repTB = mk_T_of_bnf Ds Bs bnf;
     val T_bind = qualify b;
     val TA_params = Term.add_tfreesT repTA [];
-    val TB_params = Term.add_tfreesT repTB [];
-    val ((T_name, (T_glob_info, T_loc_info)), lthy) =
-      typedef (T_bind, TA_params, NoSyn)
+    val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject)), lthy) =
+      maybe_typedef (T_bind, TA_params, NoSyn)
         (HOLogic.mk_UNIV repTA) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
-    val TA = Type (T_name, map TFree TA_params);
-    val TB = Type (T_name, map TFree TB_params);
-    val RepA = Const (#Rep_name T_glob_info, TA --> repTA);
-    val RepB = Const (#Rep_name T_glob_info, TB --> repTB);
-    val AbsA = Const (#Abs_name T_glob_info, repTA --> TA);
-    val AbsB = Const (#Abs_name T_glob_info, repTB --> TB);
-    val typedef_thm = #type_definition T_loc_info;
-    val Abs_inject' = #Abs_inject T_loc_info OF @{thms UNIV_I UNIV_I};
-    val Abs_inverse' = #Abs_inverse T_loc_info OF @{thms UNIV_I};
+
+    val repTB = mk_T_of_bnf Ds Bs bnf;
+    val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
+    val RepA = Const (Rep_name, TA --> repTA);
+    val RepB = Const (Rep_name, TB --> repTB);
+    val AbsA = Const (Abs_name, repTA --> TA);
+    val AbsB = Const (Abs_name, repTB --> TB);
+    val Abs_inject' = Abs_inject OF @{thms UNIV_I UNIV_I};
+    val Abs_inverse' = Abs_inverse OF @{thms UNIV_I};
 
     val absT_info = {absT = TA, repT = repTA, abs = AbsA, rep = RepA, abs_inject = Abs_inject',
-      abs_inverse = Abs_inverse', type_definition = typedef_thm};
+      abs_inverse = Abs_inverse', type_definition = type_definition};
 
     val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB,
       Term.list_comb (expand_maps (mk_map_of_bnf Ds As Bs bnf), fs)), RepA));
@@ -704,15 +748,16 @@
       (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
 
     fun map_id0_tac ctxt =
-      rtac (@{thm type_copy_map_id0} OF [typedef_thm, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
+      rtac (@{thm type_copy_map_id0} OF [type_definition, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
     fun map_comp0_tac ctxt =
-      rtac (@{thm type_copy_map_comp0} OF [typedef_thm, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
+      rtac (@{thm type_copy_map_comp0} OF
+        [type_definition, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
     fun map_cong0_tac ctxt =
       EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (unfold_all ctxt (map_cong0_of_bnf bnf)) ::
         map (fn i => EVERY' [select_prem_tac live (dtac meta_spec) i, etac meta_mp,
           etac (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
     fun set_map0_tac thm ctxt =
-      rtac (@{thm type_copy_set_map0} OF [typedef_thm, unfold_all ctxt thm]) 1;
+      rtac (@{thm type_copy_set_map0} OF [type_definition, unfold_all ctxt thm]) 1;
     val set_bd_tacs = map (fn thm => fn ctxt => rtac (@{thm ordLeq_ordIso_trans} OF
         [unfold_sets ctxt thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1)
       (set_bd_of_bnf bnf);
@@ -720,8 +765,9 @@
       rtac (unfold_rels ctxt (le_rel_OO_of_bnf bnf) RS @{thm vimage2p_relcompp_mono}) 1;
     fun rel_OO_Grp_tac ctxt =
       (rtac (unfold_all ctxt (rel_OO_Grp_of_bnf bnf) RS @{thm vimage2p_cong} RS trans) THEN'
-      SELECT_GOAL (unfold_thms_tac ctxt [o_apply, typedef_thm RS @{thm type_copy_vimage2p_Grp_Rep},
-        typedef_thm RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
+      SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
+        type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
+        type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
 
     val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac
       (map set_map0_tac (set_map0_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1))
@@ -732,7 +778,7 @@
           (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
       (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
-    fun wit_tac ctxt = ALLGOALS (dtac (typedef_thm RS @{thm type_copy_wit})) THEN
+    fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
       mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
 
     val (bnf', lthy') =
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -15,7 +15,7 @@
   val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
   val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
   val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
-  val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
+  val mk_comp_set_bd_tac: Proof.context -> thm option -> thm -> thm list -> tactic
   val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
   val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
 
@@ -31,6 +31,7 @@
   val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
   val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
   val mk_simple_wit_tac: thm list -> tactic
+  val bd_ordIso_natLeq_tac: tactic
 end;
 
 structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
@@ -45,7 +46,6 @@
 val trans_o_apply = @{thm trans[OF o_apply]};
 
 
-
 (* Composition *)
 
 fun mk_comp_set_alt_tac ctxt collect_set_map =
@@ -101,6 +101,7 @@
   end;
 
 fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
+  rtac @{thm natLeq_card_order} 1 ORELSE
   let
     val (card_orders, last_card_order) = split_last Fbd_card_orders;
     fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm;
@@ -111,14 +112,15 @@
   end;
 
 fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite =
-  (rtac @{thm cinfinite_cprod} THEN'
+  (rtac @{thm natLeq_cinfinite} ORELSE'
+   rtac @{thm cinfinite_cprod} THEN'
    ((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN'
      ((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE'
       rtac Fbd_cinfinite)) ORELSE'
     rtac Fbd_cinfinite) THEN'
    rtac Gbd_cinfinite) 1;
 
-fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds =
+fun mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds =
   let
     val (bds, last_bd) = split_last Gset_Fset_bds;
     fun gen_before bd =
@@ -127,6 +129,9 @@
       rtac bd;
     fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
   in
+    (case bd_ordIso_natLeq_opt of
+      SOME thm => rtac (thm RS rotate_prems 1 @{thm ordLeq_ordIso_trans}) 1
+    | NONE => all_tac) THEN
     unfold_thms_tac ctxt [comp_set_alt] THEN
     rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
     unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
@@ -168,7 +173,6 @@
     (etac FalseE ORELSE' atac))) 1);
 
 
-
 (* Kill operation *)
 
 fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
@@ -187,7 +191,6 @@
     REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1));
 
 
-
 (* Lift operation *)
 
 val empty_natural_tac = rtac @{thm empty_natural} 1;
@@ -206,7 +209,6 @@
     REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1));
 
 
-
 (* Permute operation *)
 
 fun mk_permute_in_alt_tac src dest =
@@ -214,6 +216,9 @@
   mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
     dest src) 1;
 
+
+(* Miscellaneous *)
+
 fun mk_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
   EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
 
@@ -222,4 +227,13 @@
 
 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
 
+val csum_thms =
+  @{thms csum_cong1 csum_cong2 csum_cong  csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
+val cprod_thms =
+  @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
+
+val bd_ordIso_natLeq_tac =
+  HEADGOAL (REPEAT_DETERM o resolve_tac
+    (@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms));
+
 end;
--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -90,7 +90,7 @@
 
   val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
 
-  datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
+  datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
   datatype fact_policy = Dont_Note | Note_Some | Note_All
 
   val bnf_note_all: bool Config.T
@@ -100,7 +100,7 @@
     Proof.context
 
   val print_bnfs: Proof.context -> unit
-  val prepare_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
+  val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
     binding -> binding -> binding list ->
     (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
@@ -109,7 +109,7 @@
     ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
     local_theory * thm list
 
-  val define_bnf_consts: const_policy -> fact_policy -> typ list option ->
+  val define_bnf_consts: inline_policy -> fact_policy -> typ list option ->
     binding -> binding -> binding list ->
     (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
       ((typ list * typ list * typ list * typ) *
@@ -121,7 +121,7 @@
         (typ list -> typ list -> typ list -> term) *
         (typ list -> typ list -> typ list -> term))) * local_theory
 
-  val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
+  val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     (Proof.context -> tactic) list ->
     (Proof.context -> tactic) -> typ list option -> binding ->
     binding -> binding list ->
@@ -583,7 +583,7 @@
 val rel_comppN = "rel_compp";
 val rel_compp_GrpN = "rel_compp_Grp";
 
-datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
+datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
 
 datatype fact_policy = Dont_Note | Note_Some | Note_All;
 
@@ -592,7 +592,7 @@
 
 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
 
-val smart_max_inline_size = 25; (*FUDGE*)
+val smart_max_inline_term_size = 25; (*FUDGE*)
 
 fun note_bnf_thms fact_policy qualify' bnf_b bnf =
   let
@@ -676,7 +676,7 @@
           (case const_policy of
             Dont_Inline => false
           | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
-          | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_size
+          | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_term_size
           | Do_Inline => true)
       in
         if inline then
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -20,13 +20,13 @@
      ctrXs_Tss: typ list list,
      ctr_defs: thm list,
      ctr_sugar: Ctr_Sugar.ctr_sugar,
-     co_iters: term list,
+     co_rec: term,
      maps: thm list,
      common_co_inducts: thm list,
      co_inducts: thm list,
-     co_iter_thmss: thm list list,
-     disc_co_iterss: thm list list,
-     sel_co_itersss: thm list list list};
+     co_rec_thms: thm list,
+     disc_co_recs: thm list,
+     sel_co_recss: thm list list};
 
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
   val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
@@ -41,55 +41,52 @@
   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
 
-  val mk_co_iters_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
-    typ list -> typ list -> int list -> int list list -> term list list -> Proof.context ->
-    (term list list
-     * (typ list list * typ list list list list * term list list
-        * term list list list list) list option
-     * (string * term list * term list list
-        * ((term list list * term list list list) * typ list) list) option)
-    * Proof.context
+  val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
+     typ list -> typ list -> int list -> int list list -> term list -> Proof.context ->
+     (term list
+      * (typ list list * typ list list list list * term list list * term list list list list) option
+      * (string * term list * term list list
+         * ((term list list * term list list list) * typ list)) option)
+     * Proof.context
   val repair_nullary_single_ctr: typ list list -> typ list list
-  val mk_coiter_p_pred_types: typ list -> int list -> typ list list
-  val mk_coiter_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
+  val mk_corec_p_pred_types: typ list -> int list -> typ list list
+  val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
     int list list -> term ->
     typ list list
     * (typ list list list list * typ list list list * typ list list list list * typ list)
-  val define_iters: string list ->
-    (typ list list * typ list list list list * term list list * term list list list list) list ->
-    (string -> binding) -> typ list -> typ list -> term list -> term list -> Proof.context ->
-    (term list * thm list) * Proof.context
-  val define_coiters: string list -> string * term list * term list list
-    * ((term list list * term list list list) * typ list) list ->
-    (string -> binding) -> typ list -> typ list -> term list -> term list -> Proof.context ->
-    (term list * thm list) * Proof.context
-  val derive_induct_iters_thms_for_types: BNF_Def.bnf list ->
-    (typ list list * typ list list list list * term list list * term list list list list) list ->
-    thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
-    typ list -> typ list list list -> thm list -> thm list -> thm list -> term list list ->
-    thm list list -> term list list -> thm list list -> local_theory -> lfp_sugar_thms
-  val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
-    string * term list * term list list * ((term list list * term list list list)
-      * typ list) list ->
-    thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
+  val define_rec:
+    (typ list list * typ list list list list * term list list * term list list list list) option ->
+    (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
+    (term * thm) * Proof.context
+  val define_corec: 'a * term list * term list list
+      * ((term list list * term list list list) * typ list) -> (string -> binding) -> 'b list ->
+    typ list -> term list -> term -> Proof.context -> (term * thm) * local_theory
+  val derive_induct_recs_thms_for_types: BNF_Def.bnf list ->
+     ('a * typ list list list list * term list list * 'b) option -> thm -> thm list ->
+     BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
+     typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
+     term list -> thm list -> Proof.context -> lfp_sugar_thms
+  val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list ->
+    string * term list * term list list * ((term list list * term list list list) * typ list) ->
+    thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list ->
     typ list -> typ list list list -> int list list -> int list list -> int list -> thm list ->
-    thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list list ->
-    thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
+    thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
+    thm list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
 
   type co_datatype_spec =
     ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
@@ -134,17 +131,17 @@
    ctrXs_Tss: typ list list,
    ctr_defs: thm list,
    ctr_sugar: Ctr_Sugar.ctr_sugar,
-   co_iters: term list,
+   co_rec: term,
    maps: thm list,
    common_co_inducts: thm list,
    co_inducts: thm list,
-   co_iter_thmss: thm list list,
-   disc_co_iterss: thm list list,
-   sel_co_itersss: thm list list list};
+   co_rec_thms: thm list,
+   disc_co_recs: thm list,
+   sel_co_recss: thm list list};
 
 fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
-    nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_iters, maps, common_co_inducts, co_inducts,
-    co_iter_thmss, disc_co_iterss, sel_co_itersss} : fp_sugar) =
+    nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, maps, common_co_inducts, co_inducts,
+    co_rec_thms, disc_co_recs, sel_co_recss} : fp_sugar) =
   {T = Morphism.typ phi T,
    X = Morphism.typ phi X,
    fp = fp,
@@ -157,13 +154,13 @@
    ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
    ctr_defs = map (Morphism.thm phi) ctr_defs,
    ctr_sugar = morph_ctr_sugar phi ctr_sugar,
-   co_iters = map (Morphism.term phi) co_iters,
+   co_rec = Morphism.term phi co_rec,
    maps = map (Morphism.thm phi) maps,
    common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    co_inducts = map (Morphism.thm phi) co_inducts,
-   co_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss,
-   disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss,
-   sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss};
+   co_rec_thms = map (Morphism.thm phi) co_rec_thms,
+   disc_co_recs = map (Morphism.thm phi) disc_co_recs,
+   sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss};
 
 val transfer_fp_sugar =
   morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -193,17 +190,17 @@
     (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs (fp_res as {Ts, ...})
-    ctrXs_Tsss ctr_defss ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss
-    disc_co_itersss sel_co_iterssss lthy =
+    ctrXs_Tsss ctr_defss ctr_sugars co_recs mapss common_co_inducts co_inductss co_rec_thmss
+    disc_co_recss sel_co_recsss lthy =
   (0, lthy)
   |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
     register_fp_sugar s {T = T, 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, nested_bnfs = nested_bnfs,
         nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk,
-        ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk, maps = nth mapss kk,
+        ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, maps = nth mapss kk,
         common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
-        co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
-        sel_co_itersss = nth sel_co_iterssss kk}
+        co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
+        sel_co_recss = nth sel_co_recsss kk}
       lthy)) Ts
   |> snd;
 
@@ -231,11 +228,11 @@
 
 val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
 
-fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss);
+fun flat_corec_predss_getterss qss gss = maps (op @) (qss ~~ gss);
 
-fun flat_corec_preds_predsss_gettersss [] [qss] [fss] = flat_corec_predss_getterss qss fss
-  | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
-    p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss;
+fun flat_corec_preds_predsss_gettersss [] [qss] [gss] = flat_corec_predss_getterss qss gss
+  | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (gss :: gsss) =
+    p :: flat_corec_predss_getterss qss gss @ flat_corec_preds_predsss_gettersss ps qsss gsss;
 
 fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
   Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
@@ -257,7 +254,7 @@
 val mk_ctor = mk_ctor_or_dtor range_type;
 val mk_dtor = mk_ctor_or_dtor domain_type;
 
-fun mk_co_iters thy fp fpTs Cs ts0 =
+fun mk_xtor_co_recs thy fp fpTs Cs ts0 =
   let
     val nn = length fpTs;
     val (fpTs0, Cs0) =
@@ -268,7 +265,6 @@
     map (Term.subst_TVars rho) ts0
   end;
 
-
 fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
   | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
   | unzip_recT _ T = [T];
@@ -320,11 +316,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, rec_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, rec_attrs))
   : lfp_sugar_thms;
 
 val transfer_lfp_sugar_thms =
@@ -332,233 +328,177 @@
 
 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, corec_attrs), (disc_corecss, disc_corec_attrs),
+    (disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_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, corec_attrs),
+   (map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs),
+   (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
+   (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms;
 
 val transfer_gfp_sugar_thms =
   morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
-fun mk_iters_args_types ctr_Tsss Cs absTs repTs ns mss ctor_iter_fun_Tss lthy =
+fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
   let
     val Css = map2 replicate ns Cs;
-    val y_Tsss = map5 (fn absT => fn repT => fn n => fn ms =>
-        dest_absumprodT absT repT n ms o domain_type)
-      absTs repTs ns mss (map un_fold_of ctor_iter_fun_Tss);
-    val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
-
-    val ((gss, ysss), lthy) =
-      lthy
-      |> mk_Freess "f" g_Tss
-      ||>> mk_Freesss "x" y_Tsss;
-
-    val y_Tssss = map (map (map single)) y_Tsss;
-    val yssss = map (map (map single)) ysss;
+    val x_Tssss =
+      map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T =>
+          map2 (map2 unzip_recT)
+            ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T)))
+        absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts;
 
-    val z_Tssss =
-      map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts =>
-          map2 (map2 unzip_recT)
-            ctr_Tss (dest_absumprodT absT repT n ms (domain_type (co_rec_of ctor_iter_fun_Ts))))
-        absTs repTs ns mss ctr_Tsss ctor_iter_fun_Tss;
-
-    val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
-    val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
+    val x_Tsss' = map (map flat_rec_arg_args) x_Tssss;
+    val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css;
 
-    val hss = map2 (map2 retype_free) h_Tss gss;
-    val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss;
-    val (zssss_tl, lthy) =
+    val ((fss, xssss), lthy) =
       lthy
-      |> mk_Freessss "y" (map (map (map tl)) z_Tssss);
-    val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
+      |> mk_Freess "f" f_Tss
+      ||>> mk_Freessss "x" x_Tssss;
   in
-    ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
+    ((f_Tss, x_Tssss, fss, xssss), lthy)
   end;
 
-(*avoid "'a itself" arguments in coiterators*)
+(*avoid "'a itself" arguments in corecursors*)
 fun repair_nullary_single_ctr [[]] = [[@{typ unit}]]
   | repair_nullary_single_ctr Tss = Tss;
 
-fun mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
+fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
   let
     val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
-    val f_absTs = map range_type fun_Ts;
-    val f_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss f_absTs);
-    val f_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
-      Cs ctr_Tsss' f_Tsss;
-    val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
+    val g_absTs = map range_type fun_Ts;
+    val g_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss g_absTs);
+    val g_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
+      Cs ctr_Tsss' g_Tsss;
+    val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss;
   in
-    (q_Tssss, f_Tsss, f_Tssss, f_absTs)
+    (q_Tssss, g_Tsss, g_Tssss, g_absTs)
   end;
 
-fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
+fun mk_corec_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
 
-fun mk_coiter_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_coiter =
-  (mk_coiter_p_pred_types Cs ns,
-   mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
-     (binder_fun_types (fastype_of dtor_coiter)));
-
-fun mk_coiters_args_types ctr_Tsss Cs absTs repTs ns mss dtor_coiter_fun_Tss lthy =
-  let
-    val p_Tss = mk_coiter_p_pred_types Cs ns;
+fun mk_corec_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_corec =
+  (mk_corec_p_pred_types Cs ns,
+   mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
+     (binder_fun_types (fastype_of dtor_corec)));
 
-    fun mk_types get_Ts =
-      let
-        val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
-        val (q_Tssss, f_Tsss, f_Tssss, f_repTs) =
-          mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts;
-      in
-        (q_Tssss, f_Tsss, f_Tssss, f_repTs)
-      end;
+fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy =
+  let
+    val p_Tss = mk_corec_p_pred_types Cs ns;
 
-    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 (q_Tssss, g_Tsss, g_Tssss, corec_types) =
+      mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts;
 
-    val ((((Free (z, _), cs), pss), gssss), lthy) =
+    val (((((Free (x, _), cs), pss), qssss), gssss), lthy) =
       lthy
-      |> yield_singleton (mk_Frees "z") dummyT
+      |> yield_singleton (mk_Frees "x") dummyT
       ||>> mk_Frees "a" Cs
       ||>> mk_Freess "p" p_Tss
+      ||>> mk_Freessss "q" q_Tssss
       ||>> 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 "h" (map (map (map tl)) h_Tssss);
-    val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl;
 
     val cpss = map2 (map o rapp) cs pss;
 
     fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd);
 
-    fun build_dtor_coiter_arg _ [] [cf] = cf
-      | build_dtor_coiter_arg T [cq] [cf, cf'] =
-        mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
-          (build_sum_inj Inr_const (fastype_of cf', T) $ cf');
+    fun build_dtor_corec_arg _ [] [cg] = cg
+      | build_dtor_corec_arg T [cq] [cg, cg'] =
+        mk_If cq (build_sum_inj Inl_const (fastype_of cg, T) $ cg)
+          (build_sum_inj Inr_const (fastype_of cg', T) $ cg');
 
-    fun mk_args qssss fssss f_Tsss =
-      let
-        val pfss = map3 flat_corec_preds_predsss_gettersss pss qssss fssss;
-        val cqssss = map2 (map o map o map o rapp) cs qssss;
-        val cfssss = map2 (map o map o map o rapp) cs fssss;
-        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;
+    val pgss = map3 flat_corec_preds_predsss_gettersss pss qssss gssss;
+    val cqssss = map2 (map o map o map o rapp) cs qssss;
+    val cgssss = map2 (map o map o map o rapp) cs gssss;
+    val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss;
   in
-    ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
+    ((x, cs, cpss, ((pgss, cqgsss), corec_types)), lthy)
   end;
 
-fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy =
+fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
+    val nn = length fpTs;
 
-    val (xtor_co_iter_fun_Tss, xtor_co_iterss) =
-      map (mk_co_iters thy fp fpTs Cs #> `(binder_fun_types o fastype_of o hd))
-        (transpose xtor_co_iterss0)
-      |> apsnd transpose o apfst transpose o split_list;
+    val (xtor_co_rec_fun_Ts, xtor_co_recs) =
+      mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd);
 
-    val ((iters_args_types, coiters_args_types), lthy') =
+    val ((recs_args_types, corecs_args_types), lthy') =
       if fp = Least_FP then
-        mk_iters_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_iter_fun_Tss lthy
-        |>> (rpair NONE o SOME)
+        if nn = 1 andalso forall (forall (forall (not o exists_subtype_in fpTs))) ctr_Tsss then
+          ((NONE, NONE), lthy)
+        else
+          mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
+          |>> (rpair NONE o SOME)
       else
-        mk_coiters_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_iter_fun_Tss lthy
+        mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
         |>> (pair NONE o SOME);
   in
-    ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
+    ((xtor_co_recs, recs_args_types, corecs_args_types), lthy')
   end;
 
-fun mk_preds_getterss_join c cps absT abs cqfss =
+fun mk_preds_getterss_join c cps absT abs cqgss =
   let
-    val n = length cqfss;
-    val ts = map2 (mk_absumprod absT abs n) (1 upto n) cqfss;
+    val n = length cqgss;
+    val ts = map2 (mk_absumprod absT abs n) (1 upto n) cqgss;
   in
     Term.lambda c (mk_IfN absT cps ts)
   end;
 
-fun define_co_iters fp fpT Cs binding_specs lthy0 =
+fun define_co_rec fp fpT Cs b rhs lthy0 =
   let
     val thy = Proof_Context.theory_of lthy0;
 
     val maybe_conceal_def_binding = Thm.def_binding
       #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
 
-    val ((csts, defs), (lthy', lthy)) = lthy0
-      |> apfst split_list o fold_map (fn (b, rhs) =>
-        Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
-        #>> apsnd snd) binding_specs
+    val ((cst, (_, def)), (lthy', lthy)) = lthy0
+      |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
       ||> `Local_Theory.restore;
 
     val phi = Proof_Context.export_morphism lthy lthy';
 
-    val csts' = map (mk_co_iter thy fp fpT Cs o Morphism.term phi) csts;
-    val defs' = map (Morphism.thm phi) defs;
+    val cst' = mk_co_rec thy fp fpT Cs (Morphism.term phi cst);
+    val def' = Morphism.thm phi def;
   in
-    ((csts', defs'), lthy')
-  end;
-
-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))));
-
-    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
-        (mk_binding pre,
-         fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter,
-           map4 (fn ctor_iter_absT => fn rep => fn fs => fn xsss =>
-               mk_case_absumprod ctor_iter_absT rep fs
-                 (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
-             ctor_iter_absTs reps fss xssss)))
-      end;
-  in
-    define_co_iters Least_FP fpT Cs (map3 generate_iter iterNs iter_args_typess' ctor_iters) lthy
+    ((cst', def'), lthy')
   end;
 
-fun define_coiters coiterNs (_, cs, cpss, coiter_args_typess') mk_binding fpTs Cs abss dtor_coiters
-    lthy =
+fun define_rec NONE _ _ _ _ _ = pair (Term.dummy, refl)
+  | define_rec (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_rec =
+    let
+      val nn = length fpTs;
+      val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec)
+        |>> map domain_type ||> domain_type;
+    in
+      define_co_rec Least_FP fpT Cs (mk_binding recN)
+        (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
+           map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
+               mk_case_absumprod ctor_rec_absT rep fs
+                 (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
+             ctor_rec_absTs reps fss xssss)))
+    end;
+
+fun define_corec (_, cs, cpss, ((pgss, cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
   let
     val nn = length fpTs;
-
-    val Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
-
-    fun generate_coiter pre ((pfss, cqfsss), f_absTs) dtor_coiter =
-      (mk_binding pre,
-       fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter,
-         map5 mk_preds_getterss_join cs cpss f_absTs abss cqfsss)));
+    val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
   in
-    define_co_iters Greatest_FP fpT Cs
-      (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy
+    define_co_rec Greatest_FP fpT Cs (mk_binding corecN)
+      (fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec,
+         map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
   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_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
+    nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses
+    ctrss ctr_defss recs rec_defs lthy =
   let
-    val iterss' = transpose iterss;
-    val iter_defss' = transpose iter_defss;
-
-    val [folds, recs] = iterss';
-    val [fold_defs, rec_defs] = iter_defss';
-
     val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
 
     val nn = length pre_bnfs;
@@ -668,13 +608,13 @@
 
     val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
 
-    fun mk_iter_thmss (_, x_Tssss, fss, _) iters iter_defs ctor_iter_thms =
+    fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms =
       let
-        val fiters = map (lists_bmoc fss) iters;
+        val frecs = map (lists_bmoc fss) recs;
 
-        fun mk_goal fss fiter xctr f xs fxs =
+        fun mk_goal frec xctr f xs fxs =
           fold_rev (fold_rev Logic.all) (xs :: fss)
-            (mk_Trueprop_eq (fiter $ xctr, Term.list_comb (f, fxs)));
+            (mk_Trueprop_eq (frec $ xctr, Term.list_comb (f, fxs)));
 
         fun maybe_tick (T, U) u f =
           if try (fst o HOLogic.dest_prodT) U = SOME T then
@@ -682,20 +622,19 @@
           else
             f;
 
-        fun build_iter (x as Free (_, T)) U =
+        fun build_rec (x as Free (_, T)) U =
           if T = U then
             x
           else
             build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
-              (fn kk => fn TU => maybe_tick TU (nth us kk) (nth fiters kk))) (T, U) $ x;
+              (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x;
 
-        val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_iter))) xsss x_Tssss;
-
-        val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
+        val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
+        val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
 
         val tacss =
-          map4 (map ooo mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) iter_defs)
-            ctor_iter_thms fp_abs_inverses abs_inverses ctr_defss;
+          map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs)
+            ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
 
         fun prove goal tac =
           Goal.prove_sorry lthy [] [] goal (tac o #context)
@@ -704,29 +643,24 @@
         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);
+    val rec_thmss =
+      (case rec_args_typess of
+        SOME types => mk_rec_thmss types recs rec_defs ctor_rec_thms
+      | NONE => replicate nn []);
   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), _)])
-    dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
+fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
+    dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms 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 =
+    corecs corec_defs export_args lthy =
   let
-    fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
-      iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
+    fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
+      iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]];
 
-    val ctor_dtor_coiter_thmss =
-      map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss;
-
-    val coiterss' = transpose coiterss;
-    val coiter_defss' = transpose coiter_defss;
-
-    val [unfold_defs, corec_defs] = coiter_defss';
+    val ctor_dtor_corec_thms = map3 mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms;
 
     val nn = length pre_bnfs;
 
@@ -840,79 +774,62 @@
 
     fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
 
-    val fcoiterss' as [gunfolds, hcorecs] =
-      map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss';
+    val gcorecs = map (lists_bmoc pgss) corecs;
 
-    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)
+        fun mk_goal c cps gcorec n k ctr m cfs' =
+          fold_rev (fold_rev Logic.all) ([c] :: pgss)
             (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
-               mk_Trueprop_eq (fcoiter $ c, Term.list_comb (ctr, take m cfs'))));
+               mk_Trueprop_eq (gcorec $ c, Term.list_comb (ctr, take m cfs'))));
+
+        val mk_U = typ_subst_nonatomic (map2 (fn C => fn fpT => (mk_sumT (fpT, C), fpT)) Cs fpTs);
 
-        fun mk_U maybe_mk_sumT =
-          typ_subst_nonatomic (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
-
-        fun tack z_name (c, u) f =
-          let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in
-            Term.lambda z (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ z)
+        fun tack (c, u) f =
+          let val x' = Free (x, mk_sumT (fastype_of u, fastype_of c)) in
+            Term.lambda x' (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ x')
           end;
 
-        fun build_coiter fcoiters maybe_mk_sumT maybe_tack cqf =
-          let val T = fastype_of cqf in
+        fun build_corec cqg =
+          let val T = fastype_of cqg in
             if exists_subtype_in Cs T then
-              let val U = mk_U maybe_mk_sumT T in
-                build_map lthy (indexify fst (map2 maybe_mk_sumT fpTs Cs) (fn kk => fn _ =>
-                  maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf
+              let val U = mk_U T in
+                build_map lthy (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
+                  tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg
               end
             else
-              cqf
+              cqg
           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 cqgsss' = map (map (map build_corec)) cqgsss;
+        val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
 
-        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 =
-          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;
+        val tacss =
+          map4 (map ooo mk_corec_tac corec_defs nesting_map_idents)
+            ctor_dtor_corec_thms 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),
+        fun mk_goal c cps gcorec n k disc =
+          mk_Trueprop_eq (disc $ (gcorec $ 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 gcorecs 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_corec_iff_tac) case_splitss' corec_thmss disc_thmsss;
 
         fun prove goal tac =
           Goal.prove_sorry lthy [] [] goal (tac o #context)
@@ -923,15 +840,14 @@
         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);
+    fun mk_disc_corec_thms corecs discIs = map (op RS) (corecs ~~ 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;
+    val disc_corec_thmss = map2 mk_disc_corec_thms corec_thmss discIss;
 
-    fun mk_sel_coiter_thm coiter_thm sel sel_thm =
+    fun mk_sel_corec_thm corec_thm sel sel_thm =
       let
         val (domT, ranT) = dest_funT (fastype_of sel);
         val arg_cong' =
@@ -940,14 +856,13 @@
           |> Thm.varifyT_global;
         val sel_thm' = sel_thm RSN (2, trans);
       in
-        coiter_thm RS arg_cong' RS sel_thm'
+        corec_thm RS arg_cong' RS sel_thm'
       end;
 
-    fun mk_sel_coiter_thms coiter_thmss =
-      map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss;
+    fun mk_sel_corec_thms corec_thmss =
+      map3 (map3 (map2 o mk_sel_corec_thm)) corec_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 sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
 
     val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
     val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
@@ -959,10 +874,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
@@ -1080,9 +995,9 @@
         (unsorted_As ~~ transpose set_boss);
 
     val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
-             dtors = dtors0, xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors,
+             dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
              ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
-             xtor_co_iter_thmss, ...},
+             xtor_co_rec_thms, ...},
            lthy)) =
       fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
         (map dest_TFree killed_As) fp_eqs no_defs_lthy0
@@ -1167,11 +1082,11 @@
     val kss = map (fn n => 1 upto n) ns;
     val mss = map (map length) ctr_Tsss;
 
-    val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') =
-      mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy;
+    val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
+      mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
 
     fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
-              xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
+              xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
             pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs),
           abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss),
         disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
@@ -1362,17 +1277,14 @@
 
         fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
 
-        fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
-          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);
+        fun massage_res (((maps_sets_rels, ctr_sugar), co_rec_res), lthy) =
+          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy);
       in
         (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_rec recs_args_types mk_binding fpTs Cs reps
+           else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec
          #> massage_res, lthy')
       end;
 
@@ -1381,71 +1293,71 @@
       |>> 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
+    fun derive_note_induct_recs_thms_for_types
         ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
-          (iterss, iter_defss)), lthy) =
+          (recs, rec_defs)), lthy) =
       let
-        val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, 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;
+        val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
+          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 abs_inverses type_definitions
+            abs_inverses ctrss ctr_defss recs rec_defs lthy;
 
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
 
+        val (recs', rec_thmss') =
+          if is_some recs_args_types then (recs, rec_thmss)
+          else (map #casex ctr_sugars, map #case_thms ctr_sugars);
+
         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]),
-           (recN, rec_thmss, K iter_attrs),
+          [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
+           (recN, rec_thmss, K rec_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)
+        |> (if is_some recs_args_types then
+              Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
+            else
+              I)
         |> 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 [])
+          ctrXs_Tsss ctr_defss ctr_sugars recs' mapss [induct_thm] (map single induct_thms)
+          rec_thmss' (replicate nn []) (replicate nn [])
       end;
 
-    fun derive_note_coinduct_coiters_thms_for_types
+    fun derive_note_coinduct_corecs_thms_for_types
         ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
-          (coiterss, coiter_defss)), lthy) =
+          (corecs, corec_defs)), lthy) =
       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)) =
-          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
+             (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
+             (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
+          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
+            abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
             (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;
 
-        val flat_coiter_thms = append oo append;
+        val flat_corec_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)
-            (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
+          map6 mk_simp_thms ctr_sugars
+            (map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
             mapss rel_injects rel_distincts setss;
 
         val common_notes =
@@ -1459,44 +1371,34 @@
         val notes =
           [(coinductN, map single coinduct_thms,
             fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
-           (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),
+           (corecN, corec_thmss, K corec_attrs),
+           (disc_corecN, disc_corec_thmss, K disc_corec_attrs),
+           (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
+           (sel_corecN, sel_corec_thmss, K sel_corec_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 *)
-        fun add_spec_rules coiter_of sel_thmss ctr_thmss =
-          fold (curry (Spec_Rules.add Spec_Rules.Equational) (map coiter_of coiterss))
-            [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
+        (* TODO: code theorems *)
+        |> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
+          [flat sel_corec_thmss, flat 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])
+          ctrXs_Tsss ctr_defss ctr_sugars corecs mapss [coinduct_thm, strong_coinduct_thm]
+          (transpose [coinduct_thms, strong_coinduct_thms]) corec_thmss disc_corec_thmss
+          sel_corec_thmsss
       end;
 
     val lthy'' = lthy'
       |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
-        xtor_co_iterss ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
-        pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~
-        kss ~~ mss ~~ abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~
-        ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
-        raw_sel_defaultsss)
+        xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
+        pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
+        abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
+        ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
       |> wrap_types_etc
-      |> fp_case fp derive_note_induct_iters_thms_for_types
-           derive_note_coinduct_coiters_thms_for_types;
+      |> fp_case fp derive_note_induct_recs_thms_for_types
+           derive_note_coinduct_corecs_thms_for_types;
 
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
       co_prefix fp ^ "datatype"));
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -14,16 +14,16 @@
   val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
     thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
     thm list list list -> tactic
-  val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
+  val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
   val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     tactic
-  val mk_disc_coiter_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+  val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
   val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
     thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
-  val mk_iter_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
+  val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
     tactic
 end;
 
@@ -66,7 +66,6 @@
 
 fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
   unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN
-  unfold_thms_tac ctxt @{thms split_paired_all} THEN
   HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k,
     REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n)));
 
@@ -87,32 +86,32 @@
   unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject Pair_eq conj_assoc}) THEN
   HEADGOAL (rtac refl);
 
-val iter_unfold_thms =
+val rec_unfold_thms =
   @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
       case_unit_Unity} @ sum_prod_thms_map;
 
-fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter fp_abs_inverse abs_inverse ctr_def ctxt =
-  unfold_thms_tac ctxt (ctr_def :: ctor_iter :: fp_abs_inverse :: abs_inverse :: iter_defs @
-    pre_map_defs @ map_idents @ iter_unfold_thms) THEN HEADGOAL (rtac refl);
+fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
+  unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
+    pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
 
-val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
+val corec_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
 
-fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def abs_inverse ctr_def ctxt =
+fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
   let
-    val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ coiter_unfold_thms @
+    val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ corec_unfold_thms @
       @{thms o_apply vimage2p_def if_True if_False}) ctxt;
   in
-    unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
-    HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' asm_simp_tac ss) THEN_MAYBE
+    unfold_thms_tac ctxt (ctr_def :: corec_defs) THEN
+    HEADGOAL (rtac (ctor_dtor_corec RS trans) THEN' asm_simp_tac ss) THEN_MAYBE
     HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))
   end;
 
-fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =
-  EVERY (map3 (fn case_split_tac => fn coiter_thm => fn disc =>
-      HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [coiter_thm] THEN
+fun mk_disc_corec_iff_tac case_splits' corecs discs ctxt =
+  EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
+      HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
       HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
       (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
-    (map rtac case_splits' @ [K all_tac]) coiters discs);
+    (map rtac case_splits' @ [K all_tac]) corecs discs);
 
 fun solve_prem_prem_tac ctxt =
   REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -207,7 +207,7 @@
             |> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
             |> funpow n (fn thm => thm RS spec)
             |> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
-            |> unfold_thms lthy (@{thms vimage2p_comp comp_apply comp_id
+            |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
                Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
                maps mk_fp_type_copy_thms fp_type_definitions @
                maps mk_type_copy_thms type_definitions)
@@ -236,7 +236,8 @@
       |> mk_Frees' "s" fold_strTs
       ||>> mk_Frees' "s" rec_strTs;
 
-    val co_iters = of_fp_res #xtor_co_iterss;
+    val co_folds = of_fp_res #xtor_co_folds;
+    val co_recs = of_fp_res #xtor_co_recs;
     val ns = map (length o #Ts o #fp_res) fp_sugars;
 
     fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
@@ -245,11 +246,11 @@
 
     val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
 
-    fun force_iter is_rec i TU TU_rec raw_iters =
+    fun force_iter is_rec i TU TU_rec raw_fold raw_rec =
       let
         val thy = Proof_Context.theory_of lthy;
 
-        val approx_fold = un_fold_of raw_iters
+        val approx_fold = raw_fold
           |> force_typ names_lthy
             (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
         val subst = Term.typ_subst_atomic fold_thetaAs;
@@ -269,9 +270,8 @@
 
         val js = find_indices Type.could_unify TUs cands;
         val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
-        val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
       in
-        force_typ names_lthy (Tpats ---> TU) iter
+        force_typ names_lthy (Tpats ---> TU) (if is_rec then raw_rec else raw_fold)
       end;
 
     fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
@@ -286,10 +286,11 @@
         val i = find_index (fn T => x = T) Xs;
         val TUiter =
           (case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
-            NONE => nth co_iters i
-              |> force_iter is_rec i
+            NONE => 
+              force_iter is_rec i
                 (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
-                (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
+                (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
+                (nth co_folds i) (nth co_recs i)
           | SOME f => f);
 
         val TUs = binder_fun_types (fastype_of TUiter);
@@ -373,6 +374,9 @@
     val un_folds = map (Morphism.term phi) raw_un_folds;
     val co_recs = map (Morphism.term phi) raw_co_recs;
 
+    val fp_fold_o_maps = of_fp_res #xtor_co_fold_o_map_thms;
+    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
+
     val (xtor_un_fold_thms, xtor_co_rec_thms) =
       let
         val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
@@ -419,13 +423,9 @@
 
         val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
 
-        val fp_xtor_co_iterss = of_fp_res #xtor_co_iter_thmss;
-        val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss;
-        val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss;
+        val fp_xtor_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_co_fold_thms);
+        val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
 
-        val fp_co_iter_o_mapss = of_fp_res #xtor_co_iter_o_map_thmss;
-        val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss;
-        val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss;
         val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
           map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @
           @{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
@@ -464,12 +464,8 @@
     (* These results are half broken. This is deliberate. We care only about those fields that are
        used by "primrec", "primcorecursive", and "datatype_compat". *)
     val fp_res =
-      ({Ts = fpTs,
-        bnfs = of_fp_res #bnfs,
-        dtors = dtors,
-        ctors = ctors,
-        xtor_co_iterss = transpose [un_folds, co_recs],
-        xtor_co_induct = xtor_co_induct_thm,
+      ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors, xtor_co_folds = un_folds,
+        xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
         dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
         ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
         ctor_injects = of_fp_res #ctor_injects (*too general types*),
@@ -477,9 +473,10 @@
         xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
         xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
         xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
-        xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
-        xtor_co_iter_o_map_thmss = of_fp_res #xtor_co_iter_o_map_thmss
-          (*theorem about old constant*),
+        xtor_co_fold_thms = xtor_un_fold_thms,
+        xtor_co_rec_thms = xtor_co_rec_thms,
+        xtor_co_fold_o_map_thms = fp_fold_o_maps (*theorems about old constants*),
+        xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
         rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
        |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   in
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -223,8 +223,8 @@
 
         val fp_absT_infos = map #absT_info fp_sugars0;
 
-        val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
-               dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
+        val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
+               dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
           fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
             no_defs_lthy0;
 
@@ -240,61 +240,53 @@
         val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
         val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
 
-        val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
-          mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy;
+        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;
 
         fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
 
-        val ((co_iterss, co_iter_defss), lthy) =
+        val ((co_recs, co_rec_defs), lthy) =
           fold_map2 (fn b =>
-            if fp = Least_FP then
-              define_iters [foldN, 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
+              if fp = Least_FP then define_rec recs_args_types (mk_binding b) fpTs Cs reps
+              else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
+            fp_bs xtor_co_recs 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 []))
+            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
+            |> `(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))
+            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
+              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, _)) =>
+              (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 =
+        fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec maps
+            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,
+           ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
            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_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
+           sel_co_recss = 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_recs 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 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -34,11 +34,10 @@
   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
 
-  val mk_co_iter: theory -> fp_kind -> typ -> typ list -> term -> term
+  val mk_co_rec: theory -> fp_kind -> typ -> typ list -> term -> term
 
   val mk_conjunctN: int -> int -> thm
   val conj_dests: int -> thm -> thm list
@@ -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
@@ -108,7 +104,7 @@
 
 val mk_comp = mk_compN 1;
 
-fun mk_co_iter thy fp fpT Cs t =
+fun mk_co_rec thy fp fpT Cs t =
   let
     val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last;
     val fpT0 = fp_case fp prebody body;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -13,7 +13,8 @@
      bnfs: BNF_Def.bnf list,
      ctors: term list,
      dtors: term list,
-     xtor_co_iterss: term list list,
+     xtor_co_folds: term list,
+     xtor_co_recs: term list,
      xtor_co_induct: thm,
      dtor_ctors: thm list,
      ctor_dtors: thm list,
@@ -22,16 +23,18 @@
      xtor_map_thms: thm list,
      xtor_set_thmss: thm list list,
      xtor_rel_thms: thm list,
-     xtor_co_iter_thmss: thm list list,
-     xtor_co_iter_o_map_thmss: thm list list,
+     xtor_co_fold_thms: thm list,
+     xtor_co_rec_thms: thm list,
+     xtor_co_fold_o_map_thms: thm list,
+     xtor_co_rec_o_map_thms: thm list,
      rel_xtor_co_induct_thm: thm}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
-  val un_fold_of: 'a list -> 'a
-  val co_rec_of: 'a list -> 'a
 
   val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
 
+  val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
+
   val IITN: string
   val LevN: string
   val algN: string
@@ -60,8 +63,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
@@ -85,7 +86,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
@@ -106,7 +106,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
@@ -114,7 +113,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. *)
@@ -164,7 +162,8 @@
   val mk_sum_caseN: int -> int -> thm
   val mk_sum_caseN_balanced: int -> int -> thm
 
-  val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
+  val mk_sum_Cinfinite: thm list -> thm
+  val mk_sum_card_order: thm list -> thm
 
   val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
     term list -> term list -> term list -> term list -> term list ->
@@ -195,7 +194,8 @@
    bnfs: BNF_Def.bnf list,
    ctors: term list,
    dtors: term list,
-   xtor_co_iterss: term list list,
+   xtor_co_folds: term list,
+   xtor_co_recs: term list,
    xtor_co_induct: thm,
    dtor_ctors: thm list,
    ctor_dtors: thm list,
@@ -204,18 +204,22 @@
    xtor_map_thms: thm list,
    xtor_set_thmss: thm list list,
    xtor_rel_thms: thm list,
-   xtor_co_iter_thmss: thm list list,
-   xtor_co_iter_o_map_thmss: thm list list,
+   xtor_co_fold_thms: thm list,
+   xtor_co_rec_thms: thm list,
+   xtor_co_fold_o_map_thms: thm list,
+   xtor_co_rec_o_map_thms: thm list,
    rel_xtor_co_induct_thm: thm};
 
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, dtor_ctors,
-    ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
-    xtor_co_iter_thmss, xtor_co_iter_o_map_thmss, rel_xtor_co_induct_thm} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_folds, xtor_co_recs, xtor_co_induct,
+    dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
+    xtor_rel_thms, xtor_co_fold_thms, xtor_co_rec_thms, xtor_co_fold_o_map_thms,
+    xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
   {Ts = map (Morphism.typ phi) Ts,
    bnfs = map (morph_bnf phi) bnfs,
    ctors = map (Morphism.term phi) ctors,
    dtors = map (Morphism.term phi) dtors,
-   xtor_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss,
+   xtor_co_folds = map (Morphism.term phi) xtor_co_folds,
+   xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
    xtor_co_induct = Morphism.thm phi xtor_co_induct,
    dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    ctor_dtors = map (Morphism.thm phi) ctor_dtors,
@@ -224,13 +228,12 @@
    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_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss,
-   xtor_co_iter_o_map_thmss = map (map (Morphism.thm phi)) xtor_co_iter_o_map_thmss,
+   xtor_co_fold_thms = map (Morphism.thm phi) xtor_co_fold_thms,
+   xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
+   xtor_co_fold_o_map_thms = map (Morphism.thm phi) xtor_co_fold_o_map_thms,
+   xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
    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 time ctxt timer msg = (if Config.get ctxt bnf_timing
   then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
     "ms")
@@ -322,10 +325,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
@@ -334,7 +335,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 "");
@@ -474,6 +474,12 @@
     Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)},
       right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k;
 
+fun mk_sum_Cinfinite [thm] = thm
+  | mk_sum_Cinfinite (thm :: thms) = @{thm Cinfinite_csum_weak} OF [thm, mk_sum_Cinfinite thms];
+
+fun mk_sum_card_order [thm] = thm
+  | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
+
 fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
   let
     val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -953,17 +953,8 @@
           val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
           val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
 
-          fun mk_sum_Cinfinite [thm] = thm
-            | mk_sum_Cinfinite (thm :: thms) =
-              @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
-
           val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
           val sum_Card_order = sum_Cinfinite RS conjunct2;
-
-          fun mk_sum_card_order [thm] = thm
-            | mk_sum_card_order (thm :: thms) =
-              @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
-
           val sum_card_order = mk_sum_card_order bd_card_orders;
 
           val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
@@ -2609,16 +2600,13 @@
     val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
   in
     timer;
-    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
-      xtor_co_iterss = transpose [unfolds, corecs],
-      xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
-      ctor_dtors = ctor_dtor_thms,
-      ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
+    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_folds = unfolds,
+      xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
+      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
       xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
-      xtor_rel_thms = dtor_Jrel_thms,
-      xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
-      xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_Jmap_thms, dtor_corec_o_Jmap_thms],
-      rel_xtor_co_induct_thm = Jrel_coinduct_thm},
+      xtor_rel_thms = dtor_Jrel_thms, xtor_co_fold_thms = dtor_unfold_thms,
+      xtor_co_rec_thms = dtor_corec_thms, xtor_co_fold_o_map_thms = dtor_unfold_o_Jmap_thms,
+      xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm},
      lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd)
   end;
 
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -94,7 +94,7 @@
 fun unexpected_corec_call ctxt t =
   error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
 
-fun order_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs)
+fun sort_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs);
 
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
@@ -374,9 +374,8 @@
   let
     val thy = Proof_Context.theory_of lthy0;
 
-    val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_iters = coiter1 :: _,
-            common_co_inducts = common_coinduct_thms, ...} :: _,
-          (_, gfp_sugar_thms)), lthy) =
+    val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs,
+          common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
       nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
 
     val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
@@ -394,7 +393,7 @@
 
     val perm_Ts = map #T perm_fp_sugars;
     val perm_Xs = map #X perm_fp_sugars;
-    val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o #co_iters) perm_fp_sugars;
+    val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars;
     val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
 
     fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
@@ -403,7 +402,7 @@
           SOME (T, C) => [T, C]
         | NONE => [U]);
 
-    val perm_p_Tss = mk_coiter_p_pred_types perm_Cs perm_ns';
+    val perm_p_Tss = mk_corec_p_pred_types perm_Cs perm_ns';
     val perm_f_Tssss =
       map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss';
     val perm_q_Tssss =
@@ -454,27 +453,22 @@
       end;
 
     fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
-        : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss =
-      let
-        val p_ios = map SOME p_is @ [NONE];
-        val corec_thms = co_rec_of coiter_thmss;
-        val disc_corecs = co_rec_of disc_coiterss;
-        val sel_corecss = co_rec_of sel_coitersss;
-      in
+        : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss =
+      let val p_ios = map SOME p_is @ [NONE] in
         map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
           disc_excludesss collapses corec_thms disc_corecs sel_corecss
       end;
 
-    fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters,
-        co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss,
-        sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
-      {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters),
+    fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_rec = corec,
+        co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
+        sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+      {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec,
        disc_exhausts = disc_exhausts,
        nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
        nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
-       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss
-         sel_coitersss};
+       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
+         sel_corecss};
   in
     ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
       co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
@@ -929,8 +923,8 @@
     val frees = map (fst #>> Binding.name_of #> Free) fixes;
     val has_call = exists_subterm (member (op =) frees);
     val eqns_data =
-      fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs))
-        of_specs_opt []
+      fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
+        (tag_list 0 (map snd specs)) of_specs_opt []
       |> flat o fst;
 
     val callssss =
@@ -1270,14 +1264,14 @@
         val disc_alistss = map3 (map oo prove_disc) corec_specs excludessss disc_eqnss;
         val disc_alists = map (map snd o flat) disc_alistss;
         val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
-        val disc_thmss = map (map snd o order_list_duplicates o flat) disc_alistss;
+        val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss;
         val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
-        val sel_thmss = map (map snd o order_list_duplicates) sel_alists;
+        val sel_thmss = map (map snd o sort_list_duplicates) sel_alists;
 
         fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
             (({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
-          if null exhaust_thms orelse null (tl ctr_specs) then
+          if null exhaust_thms orelse null disc_thms then
             []
           else
             let
@@ -1291,7 +1285,7 @@
                 (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
               |> K |> Goal.prove_sorry lthy [] [] goal
               |> Thm.close_derivation
-              |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
+              |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
                 @{thms eqTrueE eq_False[THEN iffD1] notnotD}
               |> pair eqn_pos
               |> single
@@ -1299,10 +1293,10 @@
 
         val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
           disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
-          |> map order_list_duplicates;
+          |> map sort_list_duplicates;
 
-        val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists) disc_eqnss
-          sel_eqnss ctr_specss;
+        val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists)
+          disc_eqnss sel_eqnss ctr_specss;
         val ctr_thmss' = map (map snd) ctr_alists;
         val ctr_thmss = map (map snd o order_list) ctr_alists;
 
@@ -1315,11 +1309,15 @@
 
         val common_name = mk_common_name fun_names;
 
+        val anonymous_notes =
+          [(flat disc_iff_or_disc_thmss, simp_attrs)]
+          |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
         val notes =
           [(coinductN, map (if n2m then single else K []) coinduct_thms, []),
            (codeN, code_thmss, code_nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
-           (discN, disc_thmss, simp_attrs),
+           (discN, disc_thmss, []),
            (disc_iffN, disc_iff_thmss, []),
            (excludeN, exclude_thmss, []),
            (exhaustN, nontriv_exhaust_thmss, []),
@@ -1343,7 +1341,7 @@
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat sel_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat ctr_thmss)
         |> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat code_thmss)
-        |> Local_Theory.notes (notes @ common_notes)
+        |> Local_Theory.notes (anonymous_notes @ notes @ common_notes)
         |> snd
       end;
 
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -587,17 +587,8 @@
           val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
           val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
 
-          fun mk_sum_Cinfinite [thm] = thm
-            | mk_sum_Cinfinite (thm :: thms) =
-              @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
-
           val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
           val sum_Card_order = sum_Cinfinite RS conjunct2;
-
-          fun mk_sum_card_order [thm] = thm
-            | mk_sum_card_order (thm :: thms) =
-              @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
-
           val sum_card_order = mk_sum_card_order bd_card_orders;
 
           val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
@@ -1863,14 +1854,13 @@
     val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
   in
     timer;
-    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
-      xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
-      ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
+    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_folds = folds,
+      xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
+      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
       xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
-      xtor_rel_thms = ctor_Irel_thms,
-      xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
-      xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_Imap_thms, ctor_rec_o_Imap_thms],
-      rel_xtor_co_induct_thm = Irel_induct_thm},
+      xtor_rel_thms = ctor_Irel_thms, xtor_co_fold_thms = ctor_fold_thms,
+      xtor_co_rec_thms = ctor_rec_thms, xtor_co_fold_o_map_thms = ctor_fold_o_Imap_thms,
+      xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm},
      lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd)
   end;
 
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -146,8 +146,8 @@
       (kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0));
 
     val descr = map3 mk_typ_descr kkssss Tparentss ctrss0;
-    val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
-    val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
+    val recs = map (fst o dest_Const o #co_rec) fp_sugars;
+    val rec_thms = maps #co_rec_thms fp_sugars;
 
     fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
         distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
@@ -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_lfp_rec_sugar.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -190,7 +190,7 @@
 
     fun mk_spec ctr_offset
         ({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
-      {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' recx,
+      {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
        nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
        ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
   in
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -21,10 +21,10 @@
 fun is_new_datatype ctxt s =
   (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
 
-fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_iters = iters,
-    co_iter_thmss = iter_thmss, ...} : fp_sugar) =
+fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_rec = recx,
+    co_rec_thms = rec_thms, ...} : fp_sugar) =
   {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs,
-   ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss};
+   ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms};
 
 fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
   let
@@ -35,7 +35,7 @@
 
     val Ts = map #T fp_sugars;
     val Xs = map #X fp_sugars;
-    val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars;
+    val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
     val Xs_TCs = Xs ~~ (Ts ~~ Cs);
 
     fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 03 15:14:00 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
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 15:14:00 2014 +0100
@@ -1775,17 +1775,24 @@
                 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
                                      \(\"" ^ s ^ "\")")
               else if is_quot_abs_fun ctxt x then
-                let
-                  val rep_T = domain_type T
-                  val abs_T = range_type T
-                in
-                  (Abs (Name.uu, rep_T,
-                        Const (@{const_name Quot}, rep_T --> abs_T)
-                               $ (Const (quot_normal_name_for_type ctxt abs_T,
-                                         rep_T --> rep_T) $ Bound 0)), ts)
-                end
+                case T of
+                  Type (@{type_name fun}, [rep_T, abs_T as Type (abs_s, _)]) =>
+                  if is_basic_datatype thy [(NONE, true)] abs_s then
+                    raise NOT_SUPPORTED ("abstraction function on " ^
+                                         quote abs_s)
+                  else
+                    (Abs (Name.uu, rep_T,
+                          Const (@{const_name Quot}, rep_T --> abs_T)
+                                 $ (Const (quot_normal_name_for_type ctxt abs_T,
+                                           rep_T --> rep_T) $ Bound 0)), ts)
               else if is_quot_rep_fun ctxt x then
-                quot_rep_of depth Ts (domain_type T) (range_type T) ts
+                case T of
+                  Type (@{type_name fun}, [abs_T as Type (abs_s, _), rep_T]) =>
+                  if is_basic_datatype thy [(NONE, true)] abs_s then
+                    raise NOT_SUPPORTED ("representation function on " ^
+                                         quote abs_s)
+                  else
+                    quot_rep_of depth Ts abs_T rep_T ts
               else if is_record_get thy x then
                 case length ts of
                   0 => (do_term depth Ts (eta_expand Ts t 1), [])
--- a/src/HOL/ex/Refute_Examples.thy	Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Mon Mar 03 15:14:00 2014 +0100
@@ -547,18 +547,6 @@
 refute [expect = genuine]
 oops
 
-lemma "rec_option n s None = n"
-refute [expect = none]
-by simp
-
-lemma "rec_option n s (Some x) = s x"
-refute [maxsize = 4, expect = none]
-by simp
-
-lemma "P (rec_option n s x)"
-refute [expect = genuine]
-oops
-
 lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
 refute [expect = genuine]
 oops