renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
authorblanchet
Fri, 21 Sep 2012 15:53:29 +0200
changeset 49504 df9b897fb254
parent 49503 dbbde075a42e
child 49505 a944eefb67e6
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
src/HOL/Codatatype/Tools/bnf_comp.ML
src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
src/HOL/Codatatype/Tools/bnf_def.ML
src/HOL/Codatatype/Tools/bnf_def_tactics.ML
src/HOL/Codatatype/Tools/bnf_fp.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
src/HOL/Codatatype/Tools/bnf_tactics.ML
src/HOL/Codatatype/Tools/bnf_util.ML
src/HOL/Codatatype/Tools/bnf_wrap.ML
src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -242,9 +242,9 @@
                  rel_converse_of_bnf outer RS sym], outer_rel_Gr],
                trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
                  (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
-          |> unfold_defs lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
+          |> unfold_thms lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
       in
-        unfold_defs_tac lthy basic_thms THEN rtac thm 1
+        unfold_thms_tac lthy basic_thms THEN rtac thm 1
       end;
 
     val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
@@ -316,7 +316,7 @@
 
     fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
     fun map_comp_tac {context, ...} =
-      unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+      unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
     fun map_cong_tac {context, ...} =
       mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
@@ -352,7 +352,7 @@
               trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
                 (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
                  replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
-          |> unfold_defs lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
+          |> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
       in
         rtac thm 1
       end;
@@ -410,7 +410,7 @@
 
     fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
     fun map_comp_tac {context, ...} =
-      unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+      unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
     fun map_cong_tac {context, ...} =
       rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
@@ -615,10 +615,10 @@
       set_unfoldss);
     val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
       pred_unfolds);
-    val unfold_maps = fold (unfold_defs lthy o single) map_unfolds;
-    val unfold_sets = fold (unfold_defs lthy) set_unfoldss;
-    val unfold_preds = unfold_defs lthy pred_unfolds;
-    val unfold_rels = unfold_defs lthy rel_unfolds;
+    val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
+    val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
+    val unfold_preds = unfold_thms lthy pred_unfolds;
+    val unfold_rels = unfold_thms lthy rel_unfolds;
     val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels;
     val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
     val bnf_sets = map (expand_maps o expand_sets)
@@ -665,7 +665,7 @@
       (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
       (mk_tac (map_wpull_of_bnf bnf))
-      (mk_tac (unfold_defs lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
+      (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -64,8 +64,8 @@
 (* Composition *)
 
 fun mk_comp_set_alt_tac ctxt collect_set_natural =
-  unfold_defs_tac ctxt @{thms sym[OF o_assoc]} THEN
-  unfold_defs_tac ctxt [collect_set_natural RS sym] THEN
+  unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
+  unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
   rtac refl 1;
 
 fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
@@ -138,9 +138,9 @@
       rtac bd;
     fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
   in
-    unfold_defs_tac ctxt [comp_set_alt] THEN
+    unfold_thms_tac ctxt [comp_set_alt] THEN
     rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
-    unfold_defs_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
+    unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
     (rtac ctrans THEN'
      WRAP' gen_before gen_after bds (rtac last_bd) THEN'
      rtac @{thm ordIso_imp_ordLeq} THEN'
@@ -152,12 +152,12 @@
   conj_assoc};
 
 fun mk_comp_in_alt_tac ctxt comp_set_alts =
-  unfold_defs_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
-  unfold_defs_tac ctxt @{thms set_eq_subset} THEN
+  unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
+  unfold_thms_tac ctxt @{thms set_eq_subset} THEN
   rtac conjI 1 THEN
   REPEAT_DETERM (
     rtac @{thm subsetI} 1 THEN
-    unfold_defs_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
+    unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
     (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
      REPEAT_DETERM (CHANGED ((
        (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE'
@@ -214,7 +214,7 @@
 
 fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms =
   ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
-  unfold_defs_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
+  unfold_thms_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
   REPEAT_DETERM (
     atac 1 ORELSE
     REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
@@ -408,7 +408,7 @@
   TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
 
 fun mk_simple_rel_O_Gr_tac ctxt rel_def rel_O_Gr in_alt_thm =
-  rtac (unfold_defs ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
+  rtac (unfold_thms ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
     1;
 
 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -1180,7 +1180,7 @@
   let
     val wits_tac =
       K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN'
-      mk_unfold_defs_then_tac lthy one_step_defs wit_tac;
+      mk_unfold_thms_then_tac lthy one_step_defs wit_tac;
     val wit_goals = map mk_conjunction_balanced' wit_goalss;
     val wit_thms =
       Skip_Proof.prove lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
@@ -1189,7 +1189,7 @@
       |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
   in
     map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
-      goals (map (mk_unfold_defs_then_tac lthy one_step_defs) tacs)
+      goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
     |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
   end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
 
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -69,8 +69,8 @@
     val n = length set_naturals;
   in
     if null set_naturals then
-      unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
-    else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+      unfold_thms_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
       EVERY' [rtac equalityI, rtac subsetI,
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
@@ -105,7 +105,7 @@
   end;
 
 fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
+  unfold_thms_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
   subst_tac ctxt [map_id] 1 THEN
     (if n = 0 then rtac refl 1
     else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
@@ -113,7 +113,7 @@
       CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
 
 fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt rel_O_Grs THEN
+  unfold_thms_tac ctxt rel_O_Grs THEN
     EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
@@ -124,8 +124,8 @@
     val n = length set_naturals;
   in
     if null set_naturals then
-      unfold_defs_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
-    else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+      unfold_thms_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
       EVERY' [rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
@@ -151,8 +151,8 @@
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
           rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
   in
-    if null set_naturals then unfold_defs_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
-    else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+    if null set_naturals then unfold_thms_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
+    else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
       EVERY' [rtac equalityI, rtac @{thm subrelI},
         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
         REPEAT_DETERM o dtac Pair_eqD,
@@ -197,7 +197,7 @@
   let
     val ls' = replicate (Int.max (1, m)) ();
   in
-    unfold_defs_tac ctxt (rel_O_Grs @
+    unfold_thms_tac ctxt (rel_O_Grs @
       @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
     EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
       rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
--- a/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -18,32 +18,30 @@
   val caseN: string
   val coN: string
   val coinductN: string
-  val coiterN: string
-  val coitersN: string
   val corecN: string
   val corecsN: string
   val ctorN: string
   val ctor_dtorN: string
-  val ctor_dtor_coitersN: string
+  val ctor_dtor_unfoldsN: string
   val ctor_dtor_corecsN: string
   val ctor_exhaustN: string
   val ctor_induct2N: string
   val ctor_inductN: string
   val ctor_injectN: string
-  val ctor_iterN: string
-  val ctor_iter_uniqueN: string
-  val ctor_itersN: string
+  val ctor_foldN: string
+  val ctor_fold_uniqueN: string
+  val ctor_foldsN: string
   val ctor_recN: string
   val ctor_recsN: string
-  val disc_coiter_iffN: string
-  val disc_coitersN: string
+  val disc_unfold_iffN: string
+  val disc_unfoldsN: string
   val disc_corec_iffN: string
   val disc_corecsN: string
   val dtorN: string
   val dtor_coinductN: string
-  val dtor_coiterN: string
-  val dtor_coiter_uniqueN: string
-  val dtor_coitersN: string
+  val dtor_unfoldN: string
+  val dtor_unfold_uniqueN: string
+  val dtor_unfoldsN: string
   val dtor_corecN: string
   val dtor_corecsN: string
   val dtor_exhaustN: string
@@ -51,13 +49,13 @@
   val dtor_injectN: string
   val dtor_strong_coinductN: string
   val exhaustN: string
+  val foldN: string
+  val foldsN: string
   val hsetN: string
   val hset_recN: string
   val inductN: string
   val injectN: string
   val isNodeN: string
-  val iterN: string
-  val itersN: string
   val lsbisN: string
   val map_simpsN: string
   val map_uniqueN: string
@@ -73,7 +71,7 @@
   val rel_simpN: string
   val rel_strong_coinductN: string
   val rvN: string
-  val sel_coitersN: string
+  val sel_unfoldsN: string
   val sel_corecsN: string
   val set_inclN: string
   val set_set_inclN: string
@@ -83,6 +81,8 @@
   val strongN: string
   val sum_bdN: string
   val sum_bdTN: string
+  val unfoldN: string
+  val unfoldsN: string
   val uniqueN: string
 
   val mk_exhaustN: string -> string
@@ -158,23 +158,24 @@
 val rawN = "raw_"
 
 val coN = "co"
+val unN = "un"
 val algN = "alg"
 val IITN = "IITN"
-val iterN = "iter"
-val itersN = iterN ^ "s"
-val coiterN = coN ^ iterN
-val coitersN = coiterN ^ "s"
+val foldN = "fold"
+val foldsN = foldN ^ "s"
+val unfoldN = unN ^ foldN
+val unfoldsN = unfoldN ^ "s"
 val uniqueN = "_unique"
 val simpsN = "simps"
 val ctorN = "ctor"
 val dtorN = "dtor"
-val ctor_iterN = ctorN ^ "_" ^ iterN
-val ctor_itersN = ctor_iterN ^ "s"
-val dtor_coiterN = dtorN ^ "_" ^ coiterN
-val dtor_coitersN = dtor_coiterN ^ "s"
-val ctor_iter_uniqueN = ctor_iterN ^ uniqueN
-val dtor_coiter_uniqueN = dtor_coiterN ^ uniqueN
-val ctor_dtor_coitersN = ctorN ^ "_" ^ dtor_coiterN ^ "s"
+val ctor_foldN = ctorN ^ "_" ^ foldN
+val ctor_foldsN = ctor_foldN ^ "s"
+val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
+val dtor_unfoldsN = dtor_unfoldN ^ "s"
+val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
+val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
+val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s"
 val map_simpsN = mapN ^ "_" ^ simpsN
 val map_uniqueN = mapN ^ uniqueN
 val min_algN = "min_alg"
@@ -237,13 +238,13 @@
 
 val caseN = "case"
 val discN = "disc"
-val disc_coitersN = discN ^ "_" ^ coitersN
+val disc_unfoldsN = discN ^ "_" ^ unfoldsN
 val disc_corecsN = discN ^ "_" ^ corecsN
 val iffN = "_iff"
-val disc_coiter_iffN = discN ^ "_" ^ coiterN ^ iffN
+val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
 val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
 val selN = "sel"
-val sel_coitersN = selN ^ "_" ^ coitersN
+val sel_unfoldsN = selN ^ "_" ^ unfoldsN
 val sel_corecsN = selN ^ "_" ^ corecsN
 
 val mk_common_name = space_implode "_";
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -169,8 +169,8 @@
     val fp_eqs =
       map dest_TFree Bs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsBs;
 
-    val (pre_bnfs, ((dtors0, ctors0, fp_iters0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
-           ctor_injects, fp_iter_thms, fp_rec_thms), lthy)) =
+    val (pre_bnfs, ((dtors0, ctors0, fp_folds0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
+           ctor_injects, fp_fold_thms, fp_rec_thms), lthy)) =
       fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
 
     fun add_nesty_bnf_names Us =
@@ -211,7 +211,7 @@
     val mss = map (map length) ctr_Tsss;
     val Css = map2 replicate ns Cs;
 
-    fun mk_iter_like Ts Us t =
+    fun mk_rec_like Ts Us t =
       let
         val (bindings, body) = strip_type (fastype_of t);
         val (f_Us, prebody) = split_last bindings;
@@ -221,20 +221,20 @@
         Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
       end;
 
-    val fp_iters as fp_iter1 :: _ = map (mk_iter_like As Cs) fp_iters0;
-    val fp_recs as fp_rec1 :: _ = map (mk_iter_like As Cs) fp_recs0;
+    val fp_folds as fp_fold1 :: _ = map (mk_rec_like As Cs) fp_folds0;
+    val fp_recs as fp_rec1 :: _ = map (mk_rec_like As Cs) fp_recs0;
 
-    val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1)));
+    val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of fp_fold1)));
     val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
 
-    val (((iter_only as (gss, _, _), rec_only as (hss, _, _)),
-          (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
+    val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
+          (zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
          names_lthy) =
       if lfp then
         let
           val y_Tsss =
             map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
-              ns mss fp_iter_fun_Ts;
+              ns mss fp_fold_fun_Ts;
           val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css;
 
           val ((gss, ysss), lthy) =
@@ -287,7 +287,7 @@
               val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
             in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end;
 
-          val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts;
+          val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_fold_fun_Ts;
 
           val ((((Free (z, _), cs), pss), gssss), lthy) =
             lthy
@@ -329,7 +329,7 @@
              (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
         end;
 
-    fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_iter), fp_rec),
+    fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_fold), fp_rec),
           ctor_dtor), dtor_ctor), ctor_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
         disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
       let
@@ -391,7 +391,7 @@
               end;
 
             val sumEN_thm' =
-              unfold_defs lthy @{thms all_unit_eq}
+              unfold_thms lthy @{thms all_unit_eq}
                 (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
                    (mk_sumEN_balanced n))
               |> Morphism.thm phi;
@@ -413,25 +413,25 @@
 
         val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
 
-        fun define_iter_rec (wrap_res, no_defs_lthy) =
+        fun define_fold_rec (wrap_res, no_defs_lthy) =
           let
             val fpT_to_C = fpT --> C;
 
-            fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) =
+            fun generate_rec_like (suf, fp_rec_like, (fss, f_Tss, xssss)) =
               let
                 val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
                 val binding = Binding.suffix_name ("_" ^ suf) fp_b;
                 val spec =
                   mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
-                    Term.list_comb (fp_iter_like,
+                    Term.list_comb (fp_rec_like,
                       map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
               in (binding, spec) end;
 
-            val iter_like_infos =
-              [(iterN, fp_iter, iter_only),
+            val rec_like_infos =
+              [(foldN, fp_fold, fold_only),
                (recN, fp_rec, rec_only)];
 
-            val (bindings, specs) = map generate_iter_like iter_like_infos |> split_list;
+            val (bindings, specs) = map generate_rec_like rec_like_infos |> split_list;
 
             val ((csts, defs), (lthy', lthy)) = no_defs_lthy
               |> apfst split_list o fold_map2 (fn b => fn spec =>
@@ -441,14 +441,14 @@
 
             val phi = Proof_Context.export_morphism lthy lthy';
 
-            val [iter_def, rec_def] = map (Morphism.thm phi) defs;
+            val [fold_def, rec_def] = map (Morphism.thm phi) defs;
 
-            val [iterx, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
+            val [foldx, recx] = map (mk_rec_like As Cs o Morphism.term phi) csts;
           in
-            ((wrap_res, ctrs, iterx, recx, xss, ctr_defs, iter_def, rec_def), lthy)
+            ((wrap_res, ctrs, foldx, recx, xss, ctr_defs, fold_def, rec_def), lthy)
           end;
 
-        fun define_coiter_corec (wrap_res, no_defs_lthy) =
+        fun define_unfold_corec (wrap_res, no_defs_lthy) =
           let
             val B_to_fpT = C --> fpT;
 
@@ -456,22 +456,22 @@
               Term.lambda c (mk_IfN sum_prod_T cps
                 (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)));
 
-            fun generate_coiter_like (suf, fp_iter_like, ((pfss, cqfsss), (f_sum_prod_Ts,
+            fun generate_corec_like (suf, fp_rec_like, ((pfss, cqfsss), (f_sum_prod_Ts,
                 pf_Tss))) =
               let
                 val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
                 val binding = Binding.suffix_name ("_" ^ suf) fp_b;
                 val spec =
                   mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
-                    Term.list_comb (fp_iter_like,
+                    Term.list_comb (fp_rec_like,
                       map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
               in (binding, spec) end;
 
-            val coiter_like_infos =
-              [(coiterN, fp_iter, coiter_only),
+            val corec_like_infos =
+              [(unfoldN, fp_fold, unfold_only),
                (corecN, fp_rec, corec_only)];
 
-            val (bindings, specs) = map generate_coiter_like coiter_like_infos |> split_list;
+            val (bindings, specs) = map generate_corec_like corec_like_infos |> split_list;
 
             val ((csts, defs), (lthy', lthy)) = no_defs_lthy
               |> apfst split_list o fold_map2 (fn b => fn spec =>
@@ -481,11 +481,11 @@
 
             val phi = Proof_Context.export_morphism lthy lthy';
 
-            val [coiter_def, corec_def] = map (Morphism.thm phi) defs;
+            val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
 
-            val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
+            val [unfold, corec] = map (mk_rec_like As Cs o Morphism.term phi) csts;
           in
-            ((wrap_res, ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy)
+            ((wrap_res, ctrs, unfold, corec, xss, ctr_defs, unfold_def, corec_def), lthy)
           end;
 
         fun wrap lthy =
@@ -494,9 +494,9 @@
               sel_defaultss))) lthy
           end;
 
-        val define_iter_likes = if lfp then define_iter_rec else define_coiter_corec;
+        val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
       in
-        ((wrap, define_iter_likes), lthy')
+        ((wrap, define_rec_likes), lthy')
       end;
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
@@ -521,11 +521,11 @@
       in Term.list_comb (mapx, args) end;
 
     val mk_simp_thmss =
-      map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn iter_likes =>
-        injects @ distincts @ cases @ rec_likes @ iter_likes);
+      map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn rec_likes =>
+        injects @ distincts @ cases @ rec_likes @ rec_likes);
 
-    fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
-        iter_defs, rec_defs), lthy) =
+    fun derive_induct_fold_rec_thms_for_types ((wrap_ress, ctrss, folds, recs, xsss, ctr_defss,
+        fold_defs, rec_defs), lthy) =
       let
         val (((phis, phis'), us'), names_lthy) =
           lthy
@@ -615,55 +615,55 @@
         (* TODO: Generate nicer names in case of clashes *)
         val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
 
-        val (iter_thmss, rec_thmss) =
+        val (fold_thmss, rec_thmss) =
           let
             val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
-            val giters = map (lists_bmoc gss) iters;
+            val gfolds = map (lists_bmoc gss) folds;
             val hrecs = map (lists_bmoc hss) recs;
 
-            fun mk_goal fss fiter_like xctr f xs fxs =
+            fun mk_goal fss frec_like xctr f xs fxs =
               fold_rev (fold_rev Logic.all) (xs :: fss)
-                (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
+                (mk_Trueprop_eq (frec_like $ xctr, Term.list_comb (f, fxs)));
 
-            fun build_call fiter_likes maybe_tick (T, U) =
+            fun build_call frec_likes maybe_tick (T, U) =
               if T = U then
                 id_const T
               else
                 (case find_index (curry (op =) T) fpTs of
-                  ~1 => build_map (build_call fiter_likes maybe_tick) T U
-                | j => maybe_tick (nth us j) (nth fiter_likes j));
+                  ~1 => build_map (build_call frec_likes maybe_tick) T U
+                | j => maybe_tick (nth us j) (nth frec_likes j));
 
             fun mk_U maybe_mk_prodT =
               typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
 
-            fun intr_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
+            fun intr_calls frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
               if member (op =) fpTs T then
-                maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
+                maybe_cons x [build_call frec_likes (K I) (T, mk_U (K I) T) $ x]
               else if exists_fp_subtype T then
-                [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
+                [build_call frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
               else
                 [x];
 
-            val gxsss = map (map (maps (intr_calls giters (K I) (K I) (K I)))) xsss;
+            val gxsss = map (map (maps (intr_calls gfolds (K I) (K I) (K I)))) xsss;
             val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
 
-            val iter_goalss = map5 (map4 o mk_goal gss) giters xctrss gss xsss gxsss;
+            val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
             val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
 
-            val iter_tacss =
-              map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms
+            val fold_tacss =
+              map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids fold_defs) fp_fold_thms
                 ctr_defss;
             val rec_tacss =
-              map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
+              map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
                 ctr_defss;
 
             fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context);
           in
-            (map2 (map2 prove) iter_goalss iter_tacss,
+            (map2 (map2 prove) fold_goalss fold_tacss,
              map2 (map2 prove) rec_goalss rec_tacss)
           end;
 
-        val simp_thmss = mk_simp_thmss wrap_ress rec_thmss iter_thmss;
+        val simp_thmss = mk_simp_thmss wrap_ress rec_thmss fold_thmss;
 
         val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
         fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
@@ -678,7 +678,7 @@
         val notes =
           [(inductN, map single induct_thms,
             fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
-           (itersN, iter_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
+           (foldsN, fold_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
            (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
            (simpsN, simp_thmss, K [])]
           |> maps (fn (thmN, thmss, attrs) =>
@@ -689,8 +689,8 @@
         lthy |> Local_Theory.notes (common_notes @ notes) |> snd
       end;
 
-    fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _,
-        ctr_defss, coiter_defs, corec_defs), lthy) =
+    fun derive_coinduct_unfold_corec_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _,
+        ctr_defss, unfold_defs, corec_defs), lthy) =
       let
         val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
         val selsss = map #2 wrap_ress;
@@ -714,79 +714,79 @@
         fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
 
         val z = the_single zs;
-        val gcoiters = map (lists_bmoc pgss) coiters;
+        val gunfolds = map (lists_bmoc pgss) unfolds;
         val hcorecs = map (lists_bmoc phss) corecs;
 
-        val (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss) =
+        val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
           let
-            fun mk_goal pfss c cps fcoiter_like n k ctr m cfs' =
+            fun mk_goal pfss c cps fcorec_like n k ctr m cfs' =
               fold_rev (fold_rev Logic.all) ([c] :: pfss)
                 (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
-                   mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
+                   mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
 
-            fun build_call fiter_likes maybe_tack (T, U) =
+            fun build_call frec_likes maybe_tack (T, U) =
               if T = U then
                 id_const T
               else
                 (case find_index (curry (op =) U) fpTs of
-                  ~1 => build_map (build_call fiter_likes maybe_tack) T U
-                | j => maybe_tack (nth cs j, nth us j) (nth fiter_likes j));
+                  ~1 => build_map (build_call frec_likes maybe_tack) T U
+                | j => maybe_tack (nth cs j, nth us j) (nth frec_likes j));
 
             fun mk_U maybe_mk_sumT =
               typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
 
-            fun intr_calls fiter_likes maybe_mk_sumT maybe_tack cqf =
+            fun intr_calls frec_likes maybe_mk_sumT maybe_tack cqf =
               let val T = fastype_of cqf in
                 if exists_subtype (member (op =) Cs) T then
-                  build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
+                  build_call frec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
                 else
                   cqf
               end;
 
-            val crgsss' = map (map (map (intr_calls gcoiters (K I) (K I)))) crgsss;
+            val crgsss' = map (map (map (intr_calls gunfolds (K I) (K I)))) crgsss;
             val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
 
-            val coiter_goalss =
-              map8 (map4 oooo mk_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
+            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 coiter_tacss =
-              map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs
+            val unfold_tacss =
+              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids) fp_fold_thms pre_map_defs
                 ctr_defss;
             val corec_tacss =
-              map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
+              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
                 ctr_defss;
 
             fun prove goal tac =
               Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation;
 
-            val coiter_thmss = map2 (map2 prove) coiter_goalss coiter_tacss;
+            val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
             val corec_thmss =
               map2 (map2 prove) corec_goalss corec_tacss
-              |> map (map (unfold_defs lthy @{thms sum_case_if}));
+              |> map (map (unfold_thms lthy @{thms sum_case_if}));
 
-            val coiter_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
+            val unfold_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
             val corec_safesss = map2 (map2 (map2 (curry (op =)))) cshsss' cshsss;
 
             val filter_safesss =
               map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
                 curry (op ~~));
 
-            val safe_coiter_thmss = filter_safesss coiter_safesss coiter_thmss;
+            val safe_unfold_thmss = filter_safesss unfold_safesss unfold_thmss;
             val safe_corec_thmss = filter_safesss corec_safesss corec_thmss;
           in
-            (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss)
+            (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
           end;
 
-        val (disc_coiter_iff_thmss, disc_corec_iff_thmss) =
+        val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
           let
-            fun mk_goal c cps fcoiter_like n k disc =
-              mk_Trueprop_eq (disc $ (fcoiter_like $ c),
+            fun mk_goal c cps fcorec_like n k disc =
+              mk_Trueprop_eq (disc $ (fcorec_like $ c),
                 if n = 1 then @{const True}
                 else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
 
-            val coiter_goalss = map6 (map2 oooo mk_goal) cs cpss gcoiters ns kss discss;
+            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;
 
             fun mk_case_split' cp =
@@ -794,10 +794,10 @@
 
             val case_splitss' = map (map mk_case_split') cpss;
 
-            val coiter_tacss =
-              map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' coiter_thmss disc_thmsss;
+            val unfold_tacss =
+              map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' unfold_thmss disc_thmsss;
             val corec_tacss =
-              map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
+              map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
 
             fun prove goal tac =
               Skip_Proof.prove lthy [] [] goal (tac o #context)
@@ -807,17 +807,17 @@
             fun proves [_] [_] = []
               | proves goals tacs = map2 prove goals tacs;
           in
-            (map2 proves coiter_goalss coiter_tacss,
+            (map2 proves unfold_goalss unfold_tacss,
              map2 proves corec_goalss corec_tacss)
           end;
 
-        fun mk_disc_coiter_like_thms coiter_likes discIs =
-          map (op RS) (filter_out (is_triv_implies o snd) (coiter_likes ~~ discIs));
+        fun mk_disc_corec_like_thms corec_likes discIs =
+          map (op RS) (filter_out (is_triv_implies o snd) (corec_likes ~~ discIs));
 
-        val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss;
-        val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss;
+        val disc_unfold_thmss = map2 mk_disc_corec_like_thms unfold_thmss discIss;
+        val disc_corec_thmss = map2 mk_disc_corec_like_thms corec_thmss discIss;
 
-        fun mk_sel_coiter_like_thm coiter_like_thm sel sel_thm =
+        fun mk_sel_corec_like_thm corec_like_thm sel sel_thm =
           let
             val (domT, ranT) = dest_funT (fastype_of sel);
             val arg_cong' =
@@ -826,25 +826,25 @@
               |> Thm.varifyT_global;
             val sel_thm' = sel_thm RSN (2, trans);
           in
-            coiter_like_thm RS arg_cong' RS sel_thm'
+            corec_like_thm RS arg_cong' RS sel_thm'
           end;
 
-        fun mk_sel_coiter_like_thms coiter_likess =
-          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_likess selsss sel_thmsss |> map flat;
+        fun mk_sel_corec_like_thms corec_likess =
+          map3 (map3 (map2 o mk_sel_corec_like_thm)) corec_likess selsss sel_thmsss |> map flat;
 
-        val sel_coiter_thmss = mk_sel_coiter_like_thms coiter_thmss;
-        val sel_corec_thmss = mk_sel_coiter_like_thms corec_thmss;
+        val sel_unfold_thmss = mk_sel_corec_like_thms unfold_thmss;
+        val sel_corec_thmss = mk_sel_corec_like_thms corec_thmss;
 
-        fun zip_coiter_like_thms coiter_likes disc_coiter_likes sel_coiter_likes =
-          coiter_likes @ disc_coiter_likes @ sel_coiter_likes;
+        fun zip_corec_like_thms corec_likes disc_corec_likes sel_corec_likes =
+          corec_likes @ disc_corec_likes @ sel_corec_likes;
 
         val simp_thmss =
           mk_simp_thmss wrap_ress
-            (map3 zip_coiter_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
-            (map3 zip_coiter_like_thms safe_coiter_thmss disc_coiter_thmss sel_coiter_thmss);
+            (map3 zip_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
+            (map3 zip_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss);
 
         val anonymous_notes =
-          [(flat safe_coiter_thmss @ flat safe_corec_thmss, simp_attrs)]
+          [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
         val common_notes =
@@ -854,13 +854,13 @@
 
         val notes =
           [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
-           (coitersN, coiter_thmss, []),
+           (unfoldsN, unfold_thmss, []),
            (corecsN, corec_thmss, []),
-           (disc_coiter_iffN, disc_coiter_iff_thmss, simp_attrs),
-           (disc_coitersN, disc_coiter_thmss, simp_attrs),
+           (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
+           (disc_unfoldsN, disc_unfold_thmss, simp_attrs),
            (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
            (disc_corecsN, disc_corec_thmss, simp_attrs),
-           (sel_coitersN, sel_coiter_thmss, simp_attrs),
+           (sel_unfoldsN, sel_unfold_thmss, simp_attrs),
            (sel_corecsN, sel_corec_thmss, simp_attrs),
            (simpsN, simp_thmss, [])]
           |> maps (fn (thmN, thmss, attrs) =>
@@ -871,16 +871,16 @@
         lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
       end;
 
-    fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
-      fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8
+    fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
+      fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list8
 
     val lthy' = lthy
-      |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_iters ~~
+      |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_folds ~~
         fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
         ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
-      |>> split_list |> wrap_types_and_define_iter_likes
-      |> (if lfp then derive_induct_iter_rec_thms_for_types
-          else derive_coinduct_coiter_corec_thms_for_types);
+      |>> split_list |> wrap_types_and_define_rec_likes
+      |> (if lfp then derive_induct_fold_rec_thms_for_types
+          else derive_coinduct_unfold_corec_thms_for_types);
 
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
       (if lfp then "" else "co") ^ "datatype"));
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -8,16 +8,16 @@
 signature BNF_FP_SUGAR_TACTICS =
 sig
   val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
-  val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
+  val mk_corec_like_tac: thm list -> thm list -> 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_like_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+  val mk_disc_corec_like_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 list -> tactic
   val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list ->
     thm -> thm list -> thm list list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> tactic
-  val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
+  val mk_rec_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
 end;
 
 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
@@ -44,14 +44,14 @@
 val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
 
 fun mk_case_tac ctxt n k m case_def ctr_def dtor_ctor =
-  unfold_defs_tac ctxt [case_def, ctr_def, dtor_ctor] THEN
+  unfold_thms_tac ctxt [case_def, ctr_def, dtor_ctor] THEN
   (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
    REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
    rtac refl) 1;
 
 fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
-  unfold_defs_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN rtac sumEN' 1 THEN
-  unfold_defs_tac ctxt @{thms all_prod_eq} THEN
+  unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN rtac sumEN' 1 THEN
+  unfold_thms_tac ctxt @{thms all_prod_eq} THEN
   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)) 1;
 
@@ -59,41 +59,41 @@
   (rtac iffI THEN'
    EVERY' (map3 (fn cTs => fn cx => fn th =>
      dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
-     SELECT_GOAL (unfold_defs_tac ctxt [th]) THEN'
+     SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
      atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])) 1;
 
 fun mk_half_distinct_tac ctxt ctor_inject ctr_defs =
-  unfold_defs_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN
+  unfold_thms_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN
   rtac @{thm sum.distinct(1)} 1;
 
 fun mk_inject_tac ctxt ctr_def ctor_inject =
-  unfold_defs_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
-  unfold_defs_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
+  unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
+  unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
-val iter_like_unfold_thms =
+val rec_like_unfold_thms =
   @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
       split_conv};
 
-fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs ctor_iter_like ctr_def ctxt =
-  unfold_defs_tac ctxt (ctr_def :: ctor_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
-    iter_like_unfold_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1;
+fun mk_rec_like_tac pre_map_defs map_ids rec_like_defs ctor_rec_like ctr_def ctxt =
+  unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_ids @
+    rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1;
 
-val coiter_like_ss = ss_only @{thms if_True if_False};
-val coiter_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
+val corec_like_ss = ss_only @{thms if_True if_False};
+val corec_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
 
-fun mk_coiter_like_tac coiter_like_defs map_ids ctor_dtor_coiter_like pre_map_def ctr_def ctxt =
-  unfold_defs_tac ctxt (ctr_def :: coiter_like_defs) THEN
-  subst_tac ctxt [ctor_dtor_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
-  unfold_defs_tac ctxt (pre_map_def :: coiter_like_unfold_thms @ map_ids) THEN
-  unfold_defs_tac ctxt @{thms id_def} THEN
+fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
+  unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
+  subst_tac ctxt [ctor_dtor_corec_like] 1 THEN asm_simp_tac corec_like_ss 1 THEN
+  unfold_thms_tac ctxt (pre_map_def :: corec_like_unfold_thms @ map_ids) THEN
+  unfold_thms_tac ctxt @{thms id_def} THEN
   TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
 
-fun mk_disc_coiter_like_iff_tac case_splits' coiter_likes discs ctxt =
-  EVERY (map3 (fn case_split_tac => fn coiter_like_thm => fn disc =>
-      case_split_tac 1 THEN unfold_defs_tac ctxt [coiter_like_thm] THEN
+fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =
+  EVERY (map3 (fn case_split_tac => fn corec_like_thm => fn disc =>
+      case_split_tac 1 THEN unfold_thms_tac ctxt [corec_like_thm] THEN
       asm_simp_tac (ss_only @{thms simp_thms(7,8,12,14,22,24)}) 1 THEN
       (if is_refl disc then all_tac else rtac disc 1))
-    (map rtac case_splits' @ [K all_tac]) coiter_likes discs);
+    (map rtac case_splits' @ [K all_tac]) corec_likes discs);
 
 val solve_prem_prem_tac =
   REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
@@ -107,7 +107,7 @@
 
 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
   EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
-     SELECT_GOAL (unfold_defs_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
+     SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
      solve_prem_prem_tac]) (rev kks)) 1;
 
 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
@@ -125,7 +125,7 @@
     val nn = length ns;
     val n = Integer.sum ns;
   in
-    unfold_defs_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
+    unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
     EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
       pre_set_defss mss (unflat mss (1 upto n)) kkss)
   end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -1060,9 +1060,9 @@
 
           val sum_card_order = mk_sum_card_order bd_card_orders;
 
-          val sbd_ordIso = fold_defs lthy [sbd_def]
+          val sbd_ordIso = fold_thms lthy [sbd_def]
             (@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order]);
-          val sbd_card_order =  fold_defs lthy [sbd_def]
+          val sbd_card_order =  fold_thms lthy [sbd_def]
             (@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]);
           val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
           val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero};
@@ -1854,14 +1854,14 @@
     val sndsTs = map snd_const prodTs;
     val dtorTs = map2 (curry (op -->)) Ts FTs;
     val ctorTs = map2 (curry (op -->)) FTs Ts;
-    val coiter_fTs = map2 (curry op -->) activeAs Ts;
+    val unfold_fTs = map2 (curry op -->) activeAs Ts;
     val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs;
     val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls;
     val corec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls_rev;
     val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls;
 
     val (((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jzs1), Jzs2), Jpairs),
-      FJzs), TRs), coiter_fs), coiter_fs_copy), corec_ss), phis), names_lthy) = names_lthy
+      FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy
       |> mk_Frees' "z" Ts
       ||>> mk_Frees' "z" Ts'
       ||>> mk_Frees "z" Ts
@@ -1870,8 +1870,8 @@
       ||>> mk_Frees "j" (map2 (curry HOLogic.mk_prodT) Ts Ts')
       ||>> mk_Frees "x" prodFTs
       ||>> mk_Frees "R" (map (mk_relT o `I) Ts)
-      ||>> mk_Frees "f" coiter_fTs
-      ||>> mk_Frees "g" coiter_fTs
+      ||>> mk_Frees "f" unfold_fTs
+      ||>> mk_Frees "g" unfold_fTs
       ||>> mk_Frees "s" corec_sTs
       ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
 
@@ -1927,38 +1927,38 @@
 
     val timer = time (timer "dtor definitions & thms");
 
-    fun coiter_bind i = Binding.suffix_name ("_" ^ dtor_coiterN) (nth bs (i - 1));
-    val coiter_name = Binding.name_of o coiter_bind;
-    val coiter_def_bind = rpair [] o Thm.def_binding o coiter_bind;
-
-    fun coiter_spec i T AT abs f z z' =
+    fun unfold_bind i = Binding.suffix_name ("_" ^ dtor_unfoldN) (nth bs (i - 1));
+    val unfold_name = Binding.name_of o unfold_bind;
+    val unfold_def_bind = rpair [] o Thm.def_binding o unfold_bind;
+
+    fun unfold_spec i T AT abs f z z' =
       let
-        val coiterT = Library.foldr (op -->) (sTs, AT --> T);
-
-        val lhs = Term.list_comb (Free (coiter_name i, coiterT), ss);
+        val unfoldT = Library.foldr (op -->) (sTs, AT --> T);
+
+        val lhs = Term.list_comb (Free (unfold_name i, unfoldT), ss);
         val rhs = Term.absfree z' (abs $ (f $ z));
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
 
-    val ((coiter_frees, (_, coiter_def_frees)), (lthy, lthy_old)) =
+    val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
       lthy
       |> fold_map7 (fn i => fn T => fn AT => fn abs => fn f => fn z => fn z' =>
         Specification.definition
-          (SOME (coiter_bind i, NONE, NoSyn), (coiter_def_bind i, coiter_spec i T AT abs f z z')))
+          (SOME (unfold_bind i, NONE, NoSyn), (unfold_def_bind i, unfold_spec i T AT abs f z z')))
           ks Ts activeAs Abs_Ts (map (fn i => HOLogic.mk_comp
             (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs zs'
       |>> apsnd split_list o split_list
       ||> `Local_Theory.restore;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
-    val coiters = map (Morphism.term phi) coiter_frees;
-    val coiter_names = map (fst o dest_Const) coiters;
-    fun mk_coiter Ts ss i = Term.list_comb (Const (nth coiter_names (i - 1), Library.foldr (op -->)
+    val unfolds = map (Morphism.term phi) unfold_frees;
+    val unfold_names = map (fst o dest_Const) unfolds;
+    fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
-    val coiter_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) coiter_def_frees;
-
-    val mor_coiter_thm =
+    val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
+
+    val mor_unfold_thm =
       let
         val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
         val morEs' = map (fn thm =>
@@ -1966,12 +1966,12 @@
       in
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all ss
-            (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_coiter Ts ss) ks))))
-          (K (mk_mor_coiter_tac m mor_UNIV_thm dtor_defs coiter_defs Abs_inverses' morEs'
+            (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
+          (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
             map_comp_id_thms map_congs))
         |> Thm.close_derivation
       end;
-    val coiter_thms = map (fn thm => (thm OF [mor_coiter_thm, UNIV_I]) RS sym) morE_thms;
+    val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
 
     val (raw_coind_thms, raw_coind_thm) =
       let
@@ -1990,15 +1990,15 @@
     val unique_mor_thms =
       let
         val prems = [HOLogic.mk_Trueprop (mk_coalg passive_UNIVs Bs ss), HOLogic.mk_Trueprop
-          (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors coiter_fs,
-            mk_mor Bs ss UNIVs dtors coiter_fs_copy))];
+          (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors unfold_fs,
+            mk_mor Bs ss UNIVs dtors unfold_fs_copy))];
         fun mk_fun_eq B f g z = HOLogic.mk_imp
           (HOLogic.mk_mem (z, B), HOLogic.mk_eq (f $ z, g $ z));
         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-          (map4 mk_fun_eq Bs coiter_fs coiter_fs_copy zs));
+          (map4 mk_fun_eq Bs unfold_fs unfold_fs_copy zs));
 
         val unique_mor = Skip_Proof.prove lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ coiter_fs @ coiter_fs_copy @ zs)
+          (fold_rev Logic.all (Bs @ ss @ unfold_fs @ unfold_fs_copy @ zs)
             (Logic.list_implies (prems, unique)))
           (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm))
           |> Thm.close_derivation;
@@ -2006,38 +2006,38 @@
         map (fn thm => conjI RSN (2, thm RS mp)) (split_conj_thm unique_mor)
       end;
 
-    val (coiter_unique_mor_thms, coiter_unique_mor_thm) =
+    val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
       let
-        val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors coiter_fs);
-        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_coiter Ts ss i);
+        val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs);
+        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_unfold Ts ss i);
         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-          (map2 mk_fun_eq coiter_fs ks));
+          (map2 mk_fun_eq unfold_fs ks));
 
         val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
         val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm];
 
         val unique_mor = Skip_Proof.prove lthy [] []
-          (fold_rev Logic.all (ss @ coiter_fs) (Logic.mk_implies (prem, unique)))
-          (K (mk_coiter_unique_mor_tac raw_coind_thms bis_thm mor_thm coiter_defs))
+          (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
+          (K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs))
           |> Thm.close_derivation;
       in
         `split_conj_thm unique_mor
       end;
 
-    val (coiter_unique_thms, coiter_unique_thm) = `split_conj_thm (split_conj_prems n
-      (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS coiter_unique_mor_thm));
-
-    val coiter_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) coiter_unique_mor_thms;
-
-    val coiter_o_dtor_thms =
+    val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n
+      (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS unfold_unique_mor_thm));
+
+    val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms;
+
+    val unfold_o_dtor_thms =
       let
-        val mor = mor_comp_thm OF [mor_str_thm, mor_coiter_thm];
+        val mor = mor_comp_thm OF [mor_str_thm, mor_unfold_thm];
       in
-        map2 (fn unique => fn coiter_ctor =>
-          trans OF [mor RS unique, coiter_ctor]) coiter_unique_mor_thms coiter_dtor_thms
+        map2 (fn unique => fn unfold_ctor =>
+          trans OF [mor RS unique, unfold_ctor]) unfold_unique_mor_thms unfold_dtor_thms
       end;
 
-    val timer = time (timer "coiter definitions & thms");
+    val timer = time (timer "unfold definitions & thms");
 
     val map_dtors = map2 (fn Ds => fn bnf =>
       Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf,
@@ -2050,7 +2050,7 @@
     fun ctor_spec i ctorT =
       let
         val lhs = Free (ctor_name i, ctorT);
-        val rhs = mk_coiter Ts map_dtors i;
+        val rhs = mk_unfold Ts map_dtors i;
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
@@ -2070,7 +2070,7 @@
     val ctors = mk_ctors params';
     val ctor_defs = map (Morphism.thm phi) ctor_def_frees;
 
-    val ctor_o_dtor_thms = map2 (fold_defs lthy o single) ctor_defs coiter_o_dtor_thms;
+    val ctor_o_dtor_thms = map2 (fold_thms lthy o single) ctor_defs unfold_o_dtor_thms;
 
     val dtor_o_ctor_thms =
       let
@@ -2078,11 +2078,11 @@
          mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
         val goals = map3 mk_goal dtors ctors FTs;
       in
-        map5 (fn goal => fn ctor_def => fn coiter => fn map_comp_id => fn map_congL =>
+        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL =>
           Skip_Proof.prove lthy [] [] goal
-            (mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtor_thms)
+            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms)
           |> Thm.close_derivation)
-          goals ctor_defs coiter_thms map_comp_id_thms map_congL_thms
+          goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms
       end;
 
     val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
@@ -2104,20 +2104,20 @@
     val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms;
     val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms;
 
-    fun mk_ctor_dtor_coiter_like_thm dtor_inject dtor_ctor coiter =
-      iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
-
-    val ctor_coiter_thms =
-      map3 mk_ctor_dtor_coiter_like_thm dtor_inject_thms dtor_ctor_thms coiter_thms;
+    fun mk_ctor_dtor_unfold_like_thm dtor_inject dtor_ctor unfold =
+      iffD1 OF [dtor_inject, trans OF [unfold, dtor_ctor RS sym]];
+
+    val ctor_dtor_unfold_thms =
+      map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_unfold_thms;
 
     val timer = time (timer "ctor definitions & thms");
 
     val corec_Inl_sum_thms =
       let
-        val mor = mor_comp_thm OF [mor_sum_case_thm, mor_coiter_thm];
+        val mor = mor_comp_thm OF [mor_sum_case_thm, mor_unfold_thm];
       in
-        map2 (fn unique => fn coiter_dtor =>
-          trans OF [mor RS unique, coiter_dtor]) coiter_unique_mor_thms coiter_dtor_thms
+        map2 (fn unique => fn unfold_dtor =>
+          trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
       end;
 
     fun corec_bind i = Binding.suffix_name ("_" ^ dtor_corecN) (nth bs (i - 1));
@@ -2132,7 +2132,7 @@
           dtors corec_ss corec_maps;
 
         val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
-        val rhs = HOLogic.mk_comp (mk_coiter Ts maps i, Inr_const T AT);
+        val rhs = HOLogic.mk_comp (mk_unfold Ts maps i, Inr_const T AT);
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
@@ -2155,7 +2155,7 @@
 
     val sum_cases =
       map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
-    val corec_thms =
+    val dtor_corec_thms =
       let
         fun mk_goal i corec_s corec_map dtor z =
           let
@@ -2166,15 +2166,15 @@
           end;
         val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
       in
-        map3 (fn goal => fn coiter => fn map_cong =>
+        map3 (fn goal => fn unfold => fn map_cong =>
           Skip_Proof.prove lthy [] [] goal
-            (mk_corec_tac m corec_defs coiter map_cong corec_Inl_sum_thms)
+            (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms)
           |> Thm.close_derivation)
-        goals coiter_thms map_congs
+        goals dtor_unfold_thms map_congs
       end;
 
-    val ctor_corec_thms =
-      map3 mk_ctor_dtor_coiter_like_thm dtor_inject_thms dtor_ctor_thms corec_thms;
+    val ctor_dtor_corec_thms =
+      map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms;
 
     val timer = time (timer "corec definitions & thms");
 
@@ -2216,7 +2216,7 @@
         val rel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
         val coinduct_params = rev (Term.add_tfrees rel_coinduct_goal []);
 
-        val rel_coinduct = unfold_defs lthy @{thms diag_UNIV}
+        val rel_coinduct = unfold_thms lthy @{thms diag_UNIV}
           (Skip_Proof.prove lthy [] [] rel_coinduct_goal
             (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm))
           |> Thm.close_derivation);
@@ -2272,8 +2272,8 @@
         val pred_of_rel_thms =
           rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
 
-        val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct;
-        val pred_strong_coinduct = unfold_defs lthy pred_of_rel_thms rel_strong_coinduct;
+        val pred_coinduct = unfold_thms lthy pred_of_rel_thms rel_coinduct;
+        val pred_strong_coinduct = unfold_thms lthy pred_of_rel_thms rel_strong_coinduct;
       in
         (dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), rel_coinduct, pred_coinduct,
          dtor_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct)
@@ -2332,7 +2332,7 @@
           map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ map mk_T Ts)) Dss bnfs;
         fun mk_Fmap mk_const fs Ts Fmap = Term.list_comb (Fmap, fs @ map mk_const Ts);
         fun mk_map mk_const mk_T Ts fs Ts' dtors mk_maps =
-          mk_coiter Ts' (map2 (fn dtor => fn Fmap =>
+          mk_unfold Ts' (map2 (fn dtor => fn Fmap =>
             HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T));
         val mk_map_id = mk_map HOLogic.id_const I;
         val mk_mapsAB = mk_maps passiveAs passiveBs;
@@ -2374,11 +2374,11 @@
             val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's;
             val cTs = map (SOME o certifyT lthy) FTs';
             val maps =
-              map5 (fn goal => fn cT => fn coiter => fn map_comp' => fn map_cong =>
+              map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong =>
                 Skip_Proof.prove lthy [] [] goal
-                  (K (mk_map_tac m n cT coiter map_comp' map_cong))
+                  (K (mk_map_tac m n cT unfold map_comp' map_cong))
                 |> Thm.close_derivation)
-              goals cTs coiter_thms map_comp's map_congs;
+              goals cTs dtor_unfold_thms map_comp's map_congs;
           in
             map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
           end;
@@ -2392,7 +2392,7 @@
                 fs_maps gs_maps fgs_maps)))
           in
             split_conj_thm (Skip_Proof.prove lthy [] [] goal
-              (K (mk_map_comp_tac m n map_thms map_comps map_congs coiter_unique_thm))
+              (K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm))
               |> Thm.close_derivation)
           end;
 
@@ -2408,7 +2408,7 @@
           in
             Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-              (mk_map_unique_tac coiter_unique_thm map_comps)
+              (mk_map_unique_tac dtor_unfold_unique_thm map_comps)
               |> Thm.close_derivation
           end;
 
@@ -2566,7 +2566,7 @@
           (map2 (curry (op $)) dtors Jzs) (map2 (curry (op $)) dtor's Jz's);
         val pickF_ss = map3 (fn pickF => fn z => fn z' =>
           HOLogic.mk_split (Term.absfree z (Term.absfree z' pickF))) pickFs Jzs' Jz's';
-        val picks = map (mk_coiter XTs pickF_ss) ks;
+        val picks = map (mk_unfold XTs pickF_ss) ks;
 
         val wpull_prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s));
@@ -2613,7 +2613,7 @@
               map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
             Skip_Proof.prove lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
               map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
-            Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def coiter_thms
+            Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms
               map_comp's) |> Thm.close_derivation)
           end;
 
@@ -2637,8 +2637,8 @@
             val thms =
               map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
                 singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal
-                  (mk_pick_col_tac m j cts rec_0s rec_Sucs coiter_thms set_natural'ss map_wpull_thms
-                    pickWP_assms_tacs))
+                  (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_natural'ss
+                    map_wpull_thms pickWP_assms_tacs))
                 |> Thm.close_derivation)
               ls goals ctss hset_rec_0ss' hset_rec_Sucss';
           in
@@ -2647,7 +2647,8 @@
 
         val timer = time (timer "helpers for BNF properties");
 
-        val map_id_tacs = map2 (K oo mk_map_id_tac map_thms) coiter_unique_thms coiter_dtor_thms;
+        val map_id_tacs =
+          map2 (K oo mk_map_id_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
         val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
         val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
         val set_nat_tacss =
@@ -2716,7 +2717,7 @@
               map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
                 ((set_minimal
                   |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y')
-                  |> unfold_defs lthy incls) OF
+                  |> unfold_thms lthy incls) OF
                   (replicate n ballI @
                     maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
                 |> singleton (Proof_Context.export names_lthy lthy)
@@ -2806,7 +2807,7 @@
           end;
 
         fun mk_coind_wits ((I, dummys), (args, thms)) =
-          ((I, dummys), (map (fn i => mk_coiter Ts args i $ HOLogic.unit) ks, thms));
+          ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms));
 
         val coind_witss =
           maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
@@ -2830,7 +2831,7 @@
           in
             map2 (fn goal => fn induct =>
               Skip_Proof.prove lthy [] [] goal
-                (mk_coind_wit_tac induct coiter_thms (flat set_natural'ss) wit_thms)
+                (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms)
               |> Thm.close_derivation)
             goals hset_induct_thms
             |> map split_conj_thm
@@ -2867,10 +2868,10 @@
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
 
-        val fold_maps = fold_defs lthy (map (fn bnf =>
+        val fold_maps = fold_thms lthy (map (fn bnf =>
           mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs);
 
-        val fold_sets = fold_defs lthy (maps (fn bnf =>
+        val fold_sets = fold_thms lthy (maps (fn bnf =>
          map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Jbnfs);
 
         val timer = time (timer "registered new codatatypes as BNFs");
@@ -2965,25 +2966,25 @@
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
       val notes =
-        [(dtor_coitersN, coiter_thms),
-        (dtor_coiter_uniqueN, coiter_unique_thms),
-        (dtor_corecsN, corec_thms),
+        [(ctor_dtorN, ctor_dtor_thms),
+        (ctor_dtor_unfoldsN, ctor_dtor_unfold_thms),
+        (ctor_dtor_corecsN, ctor_dtor_corec_thms),
+        (ctor_exhaustN, ctor_exhaust_thms),
+        (ctor_injectN, ctor_inject_thms),
+        (dtor_corecsN, dtor_corec_thms),
         (dtor_ctorN, dtor_ctor_thms),
-        (ctor_dtorN, ctor_dtor_thms),
+        (dtor_exhaustN, dtor_exhaust_thms),
         (dtor_injectN, dtor_inject_thms),
-        (dtor_exhaustN, dtor_exhaust_thms),
-        (ctor_injectN, ctor_inject_thms),
-        (ctor_exhaustN, ctor_exhaust_thms),
-        (ctor_dtor_coitersN, ctor_coiter_thms),
-        (ctor_dtor_corecsN, ctor_corec_thms)]
+        (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
+        (dtor_unfoldsN, dtor_unfold_thms)]
         |> map (apsnd (map single))
         |> maps (fn (thmN, thmss) =>
           map2 (fn b => fn thms =>
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((dtors, ctors, coiters, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
-      ctor_inject_thms, ctor_coiter_thms, ctor_corec_thms),
+    ((dtors, ctors, unfolds, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
+      ctor_inject_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -30,7 +30,6 @@
     {prems: 'a, context: Proof.context} -> tactic
   val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
-  val mk_coiter_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
     thm list list -> tactic
   val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
@@ -69,8 +68,6 @@
     thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
     thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
-  val mk_mor_coiter_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
-    thm list -> tactic
   val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
   val mk_mor_elim_tac: thm -> tactic
   val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
@@ -85,6 +82,8 @@
     {prems: thm list, context: Proof.context} -> tactic
   val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
+  val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
+    thm list -> tactic
   val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
   val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
   val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
@@ -115,6 +114,7 @@
   val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
     cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
     thm list list -> thm list list -> thm -> thm list list -> tactic
+  val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   val mk_unique_mor_tac: thm list -> thm -> tactic
   val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
@@ -345,7 +345,7 @@
 
 fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins
   {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
+  unfold_thms_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
     CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -358,7 +358,7 @@
     val n = length in_monos;
     val ks = 1 upto n;
   in
-    unfold_defs_tac ctxt [bis_def] THEN
+    unfold_thms_tac ctxt [bis_def] THEN
     EVERY' [rtac conjI,
       CONJ_WRAP' (fn i =>
         EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
@@ -421,7 +421,7 @@
           rtac conjI, etac @{thm Shift_prefCl},
           rtac conjI, rtac ballI,
             rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
-            SELECT_GOAL (unfold_defs_tac ctxt @{thms Succ_Shift shift_def}),
+            SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),
             etac bspec, etac @{thm ShiftD},
             CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
               dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
@@ -445,7 +445,7 @@
             rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
             rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
   in
-    unfold_defs_tac ctxt defs THEN
+    unfold_thms_tac ctxt defs THEN
     CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
   end;
 
@@ -598,7 +598,7 @@
     val m = length strT_hsets;
   in
     if m = 0 then atac 1
-    else (unfold_defs_tac ctxt [isNode_def] THEN
+    else (unfold_thms_tac ctxt [isNode_def] THEN
       EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
         rtac exI, rtac conjI, atac,
         CONJ_WRAP' (fn (thm, i) =>  if i > m then atac
@@ -987,7 +987,7 @@
               (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
             if n = 1 then K all_tac
             else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
-            SELECT_GOAL (unfold_defs_tac ctxt [from_to_sbd]), rtac refl,
+            SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
             rtac refl])
         ks to_sbd_injs from_to_sbds)];
   in
@@ -1044,7 +1044,7 @@
 
 fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
   {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt defs THEN
+  unfold_thms_tac ctxt defs THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
     CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
@@ -1056,21 +1056,21 @@
     (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
 
 fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt defs THEN
+  unfold_thms_tac ctxt defs THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
     CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
 
-fun mk_mor_coiter_tac m mor_UNIV dtor_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
+fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_congs =
   EVERY' [rtac iffD2, rtac mor_UNIV,
-    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, coiter_def), (map_comp_id, map_cong))) =>
+    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong))) =>
       EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
-        rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
+        rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
         rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
         rtac (o_apply RS trans RS sym), rtac map_cong,
         REPEAT_DETERM_N m o rtac refl,
-        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) coiter_defs)])
-    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ coiter_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
+        EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
+    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
 
 fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
   sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
@@ -1103,23 +1103,23 @@
       etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
   raw_coinds 1;
 
-fun mk_coiter_unique_mor_tac raw_coinds bis mor coiter_defs =
-  CONJ_WRAP' (fn (raw_coind, coiter_def) =>
+fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
+  CONJ_WRAP' (fn (raw_coind, unfold_def) =>
     EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
-      rtac @{thm image2_eqI}, rtac refl, rtac (coiter_def RS arg_cong RS trans),
-      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ coiter_defs) 1;
+      rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
+      rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
 
-fun mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtors
+fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
   {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
-    rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
+  unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
+    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
     EVERY' (map (fn thm =>
-      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_dtors),
+      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) unfold_o_dtors),
     rtac sym, rtac @{thm id_apply}] 1;
 
-fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
-    rtac trans, rtac coiter, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
+fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
+  unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
+    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
     REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
 
@@ -1179,9 +1179,9 @@
     rtac impI, REPEAT_DETERM o etac conjE,
     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
 
-fun mk_map_tac m n cT coiter map_comp' map_cong =
+fun mk_map_tac m n cT unfold map_comp' map_cong =
   EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
-    rtac (coiter RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
+    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
     REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
     REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
     rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
@@ -1201,12 +1201,12 @@
     REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
     EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
 
-fun mk_map_id_tac maps coiter_unique coiter_dtor =
-  EVERY' [rtac (coiter_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
-    rtac coiter_dtor] 1;
+fun mk_map_id_tac maps unfold_unique unfold_dtor =
+  EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
+    rtac unfold_dtor] 1;
 
-fun mk_map_comp_tac m n maps map_comps map_congs coiter_unique =
-  EVERY' [rtac coiter_unique,
+fun mk_map_comp_tac m n maps map_comps map_congs unfold_unique =
+  EVERY' [rtac unfold_unique,
     EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
       EVERY' (map rtac
         ([@{thm o_assoc} RS trans,
@@ -1255,9 +1255,9 @@
            rtac conjI, rtac refl, rtac refl]) ks]) 1
   end
 
-fun mk_map_unique_tac coiter_unique map_comps {context = ctxt, prems = _} =
-  rtac coiter_unique 1 THEN
-  unfold_defs_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
+fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
+  rtac unfold_unique 1 THEN
+  unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
   ALLGOALS (etac sym);
 
 fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
@@ -1266,11 +1266,11 @@
     val n = length map_simps;
   in
     EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
-      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_defs_tac ctxt rec_0s),
+      REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
       CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
       REPEAT_DETERM o rtac allI,
       CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
-        [SELECT_GOAL (unfold_defs_tac ctxt
+        [SELECT_GOAL (unfold_thms_tac ctxt
           (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
         rtac @{thm Un_cong}, rtac refl,
         CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
@@ -1367,14 +1367,14 @@
 
 fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
   {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt [coalg_def] THEN
+  unfold_thms_tac ctxt [coalg_def] THEN
   CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
     EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
       REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
       hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
       EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
       pickWP_assms_tac,
-      SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI,
+      SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
       REPEAT_DETERM o eresolve_tac [CollectE, conjE],
       rtac CollectI,
       REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
@@ -1389,16 +1389,16 @@
   let
     val n = length map_comps;
   in
-    unfold_defs_tac ctxt [mor_def] THEN
+    unfold_thms_tac ctxt [mor_def] THEN
     EVERY' [rtac conjI,
       CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
       CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
         EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
           REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
           hyp_subst_tac,
-          SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}),
+          SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
           rtac (map_comp RS trans),
-          SELECT_GOAL (unfold_defs_tac ctxt (conv :: @{thms o_id id_o})),
+          SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
           rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
           pickWP_assms_tac])
       (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
@@ -1407,17 +1407,17 @@
 val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
 val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
 
-fun mk_mor_thePull_pick_tac mor_def coiters map_comps {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
-  CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) coiters 1 THEN
-  CONJ_WRAP' (fn (coiter, map_comp) =>
+fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
+  unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
+  CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
+  CONJ_WRAP' (fn (unfold, map_comp) =>
     EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
       hyp_subst_tac,
-      SELECT_GOAL (unfold_defs_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})),
+      SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
       rtac refl])
-  (coiters ~~ map_comps) 1;
+  (unfolds ~~ map_comps) 1;
 
-fun mk_pick_col_tac m j cts rec_0s rec_Sucs coiters set_naturalss map_wpulls pickWP_assms_tacs
+fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_naturalss map_wpulls pickWP_assms_tacs
   {context = ctxt, prems = _} =
   let
     val n = length rec_0s;
@@ -1428,7 +1428,7 @@
       CONJ_WRAP' (fn thm => EVERY'
         [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
       REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn (rec_Suc, ((coiter, set_naturals), (map_wpull, pickWP_assms_tac))) =>
+      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_naturals), (map_wpull, pickWP_assms_tac))) =>
         EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
           REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
           hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
@@ -1437,16 +1437,16 @@
           rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
           rtac ord_eq_le_trans, rtac rec_Suc,
           rtac @{thm Un_least},
-          SELECT_GOAL (unfold_defs_tac ctxt [coiter, nth set_naturals (j - 1),
+          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_naturals (j - 1),
             @{thm prod.cases}]),
           etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
             EVERY' [rtac @{thm UN_least},
-              SELECT_GOAL (unfold_defs_tac ctxt [coiter, set_natural, @{thm prod.cases}]),
+              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_natural, @{thm prod.cases}]),
               etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
               dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
           (ks ~~ rev (drop m set_naturals))])
-      (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
+      (rec_Sucs ~~ ((unfolds ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   end;
 
 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
@@ -1477,7 +1477,7 @@
   ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
   REPEAT_DETERM (atac 1 ORELSE
     EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
-    K (unfold_defs_tac ctxt dtor_ctors),
+    K (unfold_thms_tac ctxt dtor_ctors),
     REPEAT_DETERM_N n o etac UnE,
     REPEAT_DETERM o
       (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
@@ -1485,11 +1485,11 @@
         (dresolve_tac wit THEN'
           (etac FalseE ORELSE'
           EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
-            K (unfold_defs_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
+            K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
 
-fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} =
+fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
   rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
-  unfold_defs_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN
+  unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
   ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
   ALLGOALS (TRY o
     FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -973,20 +973,20 @@
     val map_FT_inits = map2 (fn Ds =>
       mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ active_initTs)) Dss bnfs;
     val fTs = map2 (curry op -->) Ts activeAs;
-    val iterT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
+    val foldT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
     val rec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) prod_sTs;
     val rec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts;
     val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
     val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
 
     val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
-      (iter_f, iter_f')), fs), rec_ss), names_lthy) = names_lthy
+      (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy
       |> mk_Frees' "z1" Ts
       ||>> mk_Frees' "z2" Ts'
       ||>> mk_Frees' "x" FTs
       ||>> mk_Frees "y" FTs'
       ||>> mk_Freess' "z" setFTss
-      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") iterT
+      ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT
       ||>> mk_Frees "f" fTs
       ||>> mk_Frees "s" rec_sTs;
 
@@ -1049,90 +1049,90 @@
 
     val timer = time (timer "ctor definitions & thms");
 
-    val iter_fun = Term.absfree iter_f'
-      (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n iter_f) ks));
-    val iterx = HOLogic.choice_const iterT $ iter_fun;
+    val fold_fun = Term.absfree fold_f'
+      (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks));
+    val foldx = HOLogic.choice_const foldT $ fold_fun;
 
-    fun iter_bind i = Binding.suffix_name ("_" ^ ctor_iterN) (nth bs (i - 1));
-    val iter_name = Binding.name_of o iter_bind;
-    val iter_def_bind = rpair [] o Thm.def_binding o iter_bind;
+    fun fold_bind i = Binding.suffix_name ("_" ^ ctor_foldN) (nth bs (i - 1));
+    val fold_name = Binding.name_of o fold_bind;
+    val fold_def_bind = rpair [] o Thm.def_binding o fold_bind;
 
-    fun iter_spec i T AT =
+    fun fold_spec i T AT =
       let
-        val iterT = Library.foldr (op -->) (sTs, T --> AT);
+        val foldT = Library.foldr (op -->) (sTs, T --> AT);
 
-        val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
-        val rhs = mk_nthN n iterx i;
+        val lhs = Term.list_comb (Free (fold_name i, foldT), ss);
+        val rhs = mk_nthN n foldx i;
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
 
-    val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
+    val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
       lthy
       |> fold_map3 (fn i => fn T => fn AT =>
         Specification.definition
-          (SOME (iter_bind i, NONE, NoSyn), (iter_def_bind i, iter_spec i T AT)))
+          (SOME (fold_bind i, NONE, NoSyn), (fold_def_bind i, fold_spec i T AT)))
           ks Ts activeAs
       |>> apsnd split_list o split_list
       ||> `Local_Theory.restore;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
-    val iters = map (Morphism.term phi) iter_frees;
-    val iter_names = map (fst o dest_Const) iters;
-    fun mk_iter Ts ss i = Term.list_comb (Const (nth iter_names (i - 1), Library.foldr (op -->)
+    val folds = map (Morphism.term phi) fold_frees;
+    val fold_names = map (fst o dest_Const) folds;
+    fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
-    val iter_defs = map (Morphism.thm phi) iter_def_frees;
+    val fold_defs = map (Morphism.thm phi) fold_def_frees;
 
-    val mor_iter_thm =
+    val mor_fold_thm =
       let
         val ex_mor = talg_thm RS init_ex_mor_thm;
         val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
         val mor_comp = mor_Rep_thm RS mor_comp_thm;
-        val cT = certifyT lthy iterT;
-        val ct = certify lthy iter_fun
+        val cT = certifyT lthy foldT;
+        val ct = certify lthy fold_fun
       in
         singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] []
-            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_iter Ts ss) ks)))
-            (K (mk_mor_iter_tac cT ct iter_defs ex_mor (mor_comp RS mor_cong))))
+            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
+            (K (mk_mor_fold_tac cT ct fold_defs ex_mor (mor_comp RS mor_cong))))
         |> Thm.close_derivation
       end;
 
-    val iter_thms = map (fn morE => rule_by_tactic lthy
+    val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
       ((rtac CollectI THEN' CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto m + n)) 1)
-      (mor_iter_thm RS morE)) morE_thms;
+      (mor_fold_thm RS morE)) morE_thms;
 
-    val (iter_unique_mor_thms, iter_unique_mor_thm) =
+    val (fold_unique_mor_thms, fold_unique_mor_thm) =
       let
         val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs);
-        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_iter Ts ss i);
+        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i);
         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
         val unique_mor = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
-          (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms Reps
-            mor_comp_thm mor_Abs_thm mor_iter_thm))
+          (K (mk_fold_unique_mor_tac type_defs init_unique_mor_thms Reps
+            mor_comp_thm mor_Abs_thm mor_fold_thm))
           |> Thm.close_derivation;
       in
         `split_conj_thm unique_mor
       end;
 
-    val iter_unique_thms =
+    val ctor_fold_unique_thms =
       split_conj_thm (mk_conjIN n RS
-        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS iter_unique_mor_thm))
+        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS fold_unique_mor_thm))
 
-    val iter_ctor_thms =
+    val fold_ctor_thms =
       map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
-        iter_unique_mor_thms;
+        fold_unique_mor_thms;
 
-    val ctor_o_iter_thms =
+    val ctor_o_fold_thms =
       let
-        val mor = mor_comp_thm OF [mor_iter_thm, mor_str_thm];
+        val mor = mor_comp_thm OF [mor_fold_thm, mor_str_thm];
       in
-        map2 (fn unique => fn iter_ctor =>
-          trans OF [mor RS unique, iter_ctor]) iter_unique_mor_thms iter_ctor_thms
+        map2 (fn unique => fn fold_ctor =>
+          trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
       end;
 
-    val timer = time (timer "iter definitions & thms");
+    val timer = time (timer "fold definitions & thms");
 
     val map_ctors = map2 (fn Ds => fn bnf =>
       Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
@@ -1147,7 +1147,7 @@
         val dtorT = T --> FT;
 
         val lhs = Free (dtor_name i, dtorT);
-        val rhs = mk_iter Ts map_ctors i;
+        val rhs = mk_fold Ts map_ctors i;
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
@@ -1167,7 +1167,7 @@
     val dtors = mk_dtors params';
     val dtor_defs = map (Morphism.thm phi) dtor_def_frees;
 
-    val ctor_o_dtor_thms = map2 (fold_defs lthy o single) dtor_defs ctor_o_iter_thms;
+    val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms;
 
     val dtor_o_ctor_thms =
       let
@@ -1175,11 +1175,11 @@
           mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
         val goals = map3 mk_goal dtors ctors FTs;
       in
-        map5 (fn goal => fn dtor_def => fn iterx => fn map_comp_id => fn map_congL =>
+        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_congL =>
           Skip_Proof.prove lthy [] [] goal
-            (K (mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iter_thms))
+            (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_fold_thms))
           |> Thm.close_derivation)
-        goals dtor_defs iter_thms map_comp_id_thms map_congL_thms
+        goals dtor_defs ctor_fold_thms map_comp_id_thms map_congL_thms
       end;
 
     val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
@@ -1205,10 +1205,10 @@
 
     val fst_rec_pair_thms =
       let
-        val mor = mor_comp_thm OF [mor_iter_thm, mor_convol_thm];
+        val mor = mor_comp_thm OF [mor_fold_thm, mor_convol_thm];
       in
-        map2 (fn unique => fn iter_ctor =>
-          trans OF [mor RS unique, iter_ctor]) iter_unique_mor_thms iter_ctor_thms
+        map2 (fn unique => fn fold_ctor =>
+          trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
       end;
 
     fun rec_bind i = Binding.suffix_name ("_" ^ ctor_recN) (nth bs (i - 1));
@@ -1223,7 +1223,7 @@
           ctors rec_ss rec_maps;
 
         val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
-        val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_iter Ts maps i);
+        val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts maps i);
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
@@ -1245,7 +1245,7 @@
     val rec_defs = map (Morphism.thm phi) rec_def_frees;
 
     val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
-    val rec_thms =
+    val ctor_rec_thms =
       let
         fun mk_goal i rec_s rec_map ctor x =
           let
@@ -1256,10 +1256,10 @@
           end;
         val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
       in
-        map2 (fn goal => fn iterx =>
-          Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iterx fst_rec_pair_thms)
+        map2 (fn goal => fn foldx =>
+          Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs foldx fst_rec_pair_thms)
           |> Thm.close_derivation)
-        goals iter_thms
+        goals ctor_fold_thms
       end;
 
     val timer = time (timer "rec definitions & thms");
@@ -1381,10 +1381,10 @@
           mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         fun mk_passive_maps ATs BTs Ts =
           map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ Ts)) Dss bnfs;
-        fun mk_map_iter_arg fs Ts ctor fmap =
+        fun mk_map_fold_arg fs Ts ctor fmap =
           HOLogic.mk_comp (ctor, Term.list_comb (fmap, fs @ map HOLogic.id_const Ts));
         fun mk_map Ts fs Ts' ctors mk_maps =
-          mk_iter Ts (map2 (mk_map_iter_arg fs Ts') ctors (mk_maps Ts'));
+          mk_fold Ts (map2 (mk_map_fold_arg fs Ts') ctors (mk_maps Ts'));
         val pmapsABT' = mk_passive_maps passiveAs passiveBs;
         val fs_maps = map (mk_map Ts fs Ts' ctor's pmapsABT') ks;
         val fs_copy_maps = map (mk_map Ts fs_copy Ts' ctor's pmapsABT') ks;
@@ -1401,10 +1401,10 @@
                 HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps))));
             val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
             val maps =
-              map4 (fn goal => fn iterx => fn map_comp_id => fn map_cong =>
-                Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iterx map_comp_id map_cong))
+              map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong =>
+                Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong))
                 |> Thm.close_derivation)
-              goals iter_thms map_comp_id_thms map_congs;
+              goals ctor_fold_thms map_comp_id_thms map_congs;
           in
             map (fn thm => thm RS @{thm pointfreeE}) maps
           end;
@@ -1420,7 +1420,7 @@
                 (map2 (curry HOLogic.mk_eq) us fs_maps));
             val unique = Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-              (K (mk_map_unique_tac m mor_def iter_unique_mor_thm map_comp_id_thms map_congs))
+              (K (mk_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
               |> Thm.close_derivation;
           in
             `split_conj_thm unique
@@ -1451,7 +1451,7 @@
           end;
 
         val colss = map5 (fn l => fn T => map3 (mk_col l T)) ls passiveAs AFss AFss' setsss;
-        val setss_by_range = map (fn cols => map (mk_iter Ts cols) ks) colss;
+        val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
         val setss_by_bnf = transpose setss_by_range;
 
         val set_simp_thmss =
@@ -1461,9 +1461,9 @@
                 HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
             val goalss =
               map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss;
-            val setss = map (map2 (fn iterx => fn goal =>
-              Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iterx)) |> Thm.close_derivation)
-              iter_thms) goalss;
+            val setss = map (map2 (fn foldx => fn goal =>
+              Skip_Proof.prove lthy [] [] goal (K (mk_set_tac foldx)) |> Thm.close_derivation)
+              ctor_fold_thms) goalss;
 
             fun mk_simp_goal pas_set act_sets sets ctor z set =
               Logic.all z (mk_Trueprop_eq (set $ (ctor $ z),
@@ -1712,11 +1712,11 @@
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;
 
-        val fold_maps = fold_defs lthy (map (fn bnf =>
+        val fold_maps = fold_thms lthy (map (fn bnf =>
           mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs);
 
-        val fold_sets = fold_defs lthy (maps (fn bnf =>
-         map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
+        val fold_sets = fold_thms lthy (maps (fn bnf =>
+          map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
 
         val timer = time (timer "registered new datatypes as BNFs");
 
@@ -1806,10 +1806,10 @@
       val notes =
         [(ctor_dtorN, ctor_dtor_thms),
         (ctor_exhaustN, ctor_exhaust_thms),
+        (ctor_fold_uniqueN, ctor_fold_unique_thms),
+        (ctor_foldsN, ctor_fold_thms),
         (ctor_injectN, ctor_inject_thms),
-        (ctor_iter_uniqueN, iter_unique_thms),
-        (ctor_itersN, iter_thms),
-        (ctor_recsN, rec_thms),
+        (ctor_recsN, ctor_rec_thms),
         (dtor_ctorN, dtor_ctor_thms),
         (dtor_exhaustN, dtor_exhaust_thms),
         (dtor_injectN, dtor_inject_thms)]
@@ -1819,8 +1819,8 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((dtors, ctors, iters, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms,
-      iter_thms, rec_thms),
+    ((dtors, ctors, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms,
+      ctor_fold_thms, ctor_rec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -32,7 +32,7 @@
   val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
     thm list -> tactic
   val mk_iso_alt_tac: thm list -> thm -> tactic
-  val mk_iter_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
+  val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
   val mk_least_min_alg_tac: thm -> thm -> tactic
   val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list ->
     thm list list list -> thm list -> tactic
@@ -56,7 +56,7 @@
   val mk_mor_elim_tac: thm -> tactic
   val mk_mor_incl_tac: thm -> thm list -> tactic
   val mk_mor_inv_tac: thm -> thm -> thm list list -> thm list -> thm list -> thm list -> tactic
-  val mk_mor_iter_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
+  val mk_mor_fold_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
   val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
     thm list -> tactic
   val mk_mor_str_tac: 'a list -> thm -> tactic
@@ -386,7 +386,7 @@
 
 fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
   EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
-  unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
+  unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
 
 fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
     alg_sets set_natural's str_init_defs =
@@ -431,7 +431,7 @@
     rtac mor_select THEN' atac THEN' rtac CollectI THEN'
     REPEAT_DETERM o rtac exI THEN'
     rtac conjI THEN' rtac refl THEN' atac THEN'
-    K (unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
+    K (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
     etac mor_comp THEN' etac mor_incl_min_alg) 1
   end;
 
@@ -486,7 +486,7 @@
   end;
 
 fun mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
-  (K (unfold_defs_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
+  (K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
   EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
   EVERY' (map rtac inver_Abss) THEN'
   EVERY' (map rtac inver_Reps)) 1;
@@ -497,34 +497,34 @@
     EVERY' [rtac conjI, rtac subset_UNIV, rtac conjI, rtac inver_Rep, rtac inver_Abs])
     inver_Abss inver_Reps)) 1;
 
-fun mk_mor_iter_tac cT ct iter_defs ex_mor mor =
-  (EVERY' (map stac iter_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
-  REPEAT_DETERM_N (length iter_defs) o etac exE THEN'
+fun mk_mor_fold_tac cT ct fold_defs ex_mor mor =
+  (EVERY' (map stac fold_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
+  REPEAT_DETERM_N (length fold_defs) o etac exE THEN'
   rtac (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac mor) 1;
 
-fun mk_iter_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_iter =
+fun mk_fold_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold =
   let
     fun mk_unique type_def =
       EVERY' [rtac @{thm surj_fun_eq}, rtac (type_def RS @{thm type_definition.Abs_image}),
         rtac ballI, resolve_tac init_unique_mors,
         EVERY' (map (fn thm => atac ORELSE' rtac thm) Reps),
         rtac mor_comp, rtac mor_Abs, atac,
-        rtac mor_comp, rtac mor_Abs, rtac mor_iter];
+        rtac mor_comp, rtac mor_Abs, rtac mor_fold];
   in
     CONJ_WRAP' mk_unique type_defs 1
   end;
 
-fun mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iters =
-  EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx,
+fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_folds =
+  EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
     rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
     EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
-      ctor_o_iters),
+      ctor_o_folds),
     rtac sym, rtac id_apply] 1;
 
-fun mk_rec_tac rec_defs iterx fst_recs {context = ctxt, prems = _}=
-  unfold_defs_tac ctxt
+fun mk_rec_tac rec_defs foldx fst_recs {context = ctxt, prems = _}=
+  unfold_thms_tac ctxt
     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
-  EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iterx RS @{thm arg_cong[of _ _ snd]}),
+  EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}),
     rtac @{thm snd_convol'}] 1;
 
 fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
@@ -570,14 +570,14 @@
       CONJ_WRAP' (K atac) ks] 1
   end;
 
-fun mk_map_tac m n iterx map_comp_id map_cong =
-  EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx, rtac trans, rtac o_apply,
+fun mk_map_tac m n foldx map_comp_id map_cong =
+  EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
     rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong),
     REPEAT_DETERM_N m o rtac refl,
     REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
     rtac sym, rtac o_apply] 1;
 
-fun mk_map_unique_tac m mor_def iter_unique_mor map_comp_ids map_congs =
+fun mk_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs =
   let
     val n = length map_congs;
     fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
@@ -586,13 +586,13 @@
       REPEAT_DETERM_N m o rtac refl,
       REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
   in
-    EVERY' [rtac iter_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
+    EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
       CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_congs,
       CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1
   end;
 
-fun mk_set_tac iterx = EVERY' [rtac ext, rtac trans, rtac o_apply,
-  rtac trans, rtac iterx, rtac sym, rtac o_apply] 1;
+fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
+  rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
 
 fun mk_set_simp_tac set set_natural' set_natural's =
   let
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -16,8 +16,8 @@
   val subst_asm_tac: Proof.context -> thm list -> int -> tactic
   val subst_tac: Proof.context -> thm list -> int -> tactic
   val substs_tac: Proof.context -> thm list -> int -> tactic
-  val unfold_defs_tac: Proof.context -> thm list -> tactic
-  val mk_unfold_defs_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
+  val unfold_thms_tac: Proof.context -> thm list -> tactic
+  val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
 
   val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
   val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
@@ -57,11 +57,11 @@
     rtac (Drule.instantiate_normalize insts thm) 1
   end);
 
-fun unfold_defs_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
+fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
 
-fun mk_unfold_defs_then_tac lthy defs tac x = unfold_defs_tac lthy defs THEN tac x;
+fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
 
-(*unlike "unfold_defs_tac", succeeds when the RHS contains schematic variables not in the LHS*)
+(*unlike "unfold_thms_tac", succeeds when the RHS contains schematic variables not in the LHS*)
 fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
 fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
 fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
@@ -99,13 +99,13 @@
   end;
 
 fun simple_rel_O_Gr_tac ctxt =
-  unfold_defs_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
+  unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
 
 fun mk_pred_simp_tac rel_def IJpred_defs IJrel_defs rel_simp {context = ctxt, prems = _} =
-  unfold_defs_tac ctxt IJpred_defs THEN
-  subst_tac ctxt [unfold_defs ctxt (IJpred_defs @ IJrel_defs @
+  unfold_thms_tac ctxt IJpred_defs THEN
+  subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJrel_defs @
     @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) rel_simp] 1 THEN
-  unfold_defs_tac ctxt (rel_def ::
+  unfold_thms_tac ctxt (rel_def ::
     @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
       split_conv}) THEN
   rtac refl 1;
--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -134,8 +134,8 @@
   val no_refl: thm list -> thm list
   val no_reflexive: thm list -> thm list
 
-  val fold_defs: Proof.context -> thm list -> thm -> thm
-  val unfold_defs: Proof.context -> thm list -> thm -> thm
+  val fold_thms: Proof.context -> thm list -> thm -> thm
+  val unfold_thms: Proof.context -> thm list -> thm -> thm
 
   val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
   val find_indices: ''a list -> ''a list -> int list
@@ -613,7 +613,7 @@
 val no_refl = filter_out is_refl;
 val no_reflexive = filter_out Thm.is_reflexive;
 
-fun fold_defs ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
-fun unfold_defs ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
+fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
+fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
 
 end;
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -443,7 +443,7 @@
                   disc_defs';
               val not_discI_thms =
                 map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
-                    (unfold_defs lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
+                    (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
                   ms disc_defs';
 
               val (disc_thmss', disc_thmss) =
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -42,7 +42,7 @@
 
 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
   EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
-    hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
+    hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
     rtac distinct, rtac uexhaust] @
     (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
      |> k = 1 ? swap |> op @)) 1;
@@ -63,7 +63,7 @@
       atac
     else
       REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
-      SELECT_GOAL (unfold_defs_tac ctxt sels) THEN' rtac refl)) 1;
+      SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
 
 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
     disc_excludesss' =
@@ -98,7 +98,7 @@
 fun mk_case_eq_tac ctxt n uexhaust cases discss' selss =
   (rtac uexhaust THEN'
    EVERY' (map3 (fn casex => fn if_discs => fn sels =>
-       EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_discs @ sels)), rtac casex])
+       EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
      cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
 
 fun mk_case_cong_tac uexhaust cases =
@@ -117,6 +117,6 @@
 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
 
 fun mk_split_asm_tac ctxt split =
-  rtac (split RS trans) 1 THEN unfold_defs_tac ctxt split_asm_thms THEN rtac refl 1;
+  rtac (split RS trans) 1 THEN unfold_thms_tac ctxt split_asm_thms THEN rtac refl 1;
 
 end;