# HG changeset patch
# User wenzelm
# Date 1392753613 -3600
# Node ID 439d40b226d1a4ab707ae1f7d8e9026f3a275166
# Parent  4394bb0b522b5bfd8e6b142cff8682b7f4b38ea5# Parent  88c40aff747dee1fad7a099ca19fbe2472fdb425
merged

diff -r 88c40aff747d -r 439d40b226d1 src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Tue Feb 18 21:00:13 2014 +0100
@@ -154,6 +154,5 @@
 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
 ML_file "Tools/BNF/bnf_fp_n2m.ML"
 ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
-ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
 
 end
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/BNF_GFP.thy	Tue Feb 18 21:00:13 2014 +0100
@@ -51,21 +51,6 @@
 (* Operators: *)
 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
 
-lemma Id_onD: "(a, b) \<in> Id_on A \<Longrightarrow> a = b"
-unfolding Id_on_def by simp
-
-lemma Id_onD': "x \<in> Id_on A \<Longrightarrow> fst x = snd x"
-unfolding Id_on_def by auto
-
-lemma Id_on_fst: "x \<in> Id_on A \<Longrightarrow> fst x \<in> A"
-unfolding Id_on_def by auto
-
-lemma Id_on_UNIV: "Id_on UNIV = Id"
-unfolding Id_on_def by auto
-
-lemma Id_on_Comp: "Id_on A = Id_on A O Id_on A"
-unfolding Id_on_def by auto
-
 lemma Id_on_Gr: "Id_on A = Gr A id"
 unfolding Id_on_def Gr_def by auto
 
@@ -102,9 +87,6 @@
 lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
 by force
 
-lemma Collect_split_in_relI: "x \<in> X \<Longrightarrow> x \<in> Collect (split (in_rel X))"
-by auto
-
 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
 unfolding fun_eq_iff by auto
 
@@ -114,9 +96,6 @@
 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
 unfolding Gr_def Grp_def fun_eq_iff by auto
 
-lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op ="
-unfolding fun_eq_iff by auto
-
 definition relImage where
 "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
 
@@ -349,10 +328,10 @@
   thus "univ f X \<in> B" using x PRES by simp
 qed
 
-ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
 ML_file "Tools/BNF/bnf_gfp_util.ML"
 ML_file "Tools/BNF/bnf_gfp_tactics.ML"
 ML_file "Tools/BNF/bnf_gfp.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
 
 end
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Tue Feb 18 21:00:13 2014 +0100
@@ -237,11 +237,12 @@
 lemma id_transfer: "fun_rel A A id id"
 unfolding fun_rel_def by simp
 
-ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
 ML_file "Tools/BNF/bnf_lfp_util.ML"
 ML_file "Tools/BNF/bnf_lfp_tactics.ML"
 ML_file "Tools/BNF/bnf_lfp.ML"
 ML_file "Tools/BNF/bnf_lfp_compat.ML"
+ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
+ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
 
 hide_fact (open) id_transfer
 
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Nitpick.thy	Tue Feb 18 21:00:13 2014 +0100
@@ -9,7 +9,9 @@
 
 theory Nitpick
 imports BNF_FP_Base Map Record Sledgehammer
-keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
+keywords
+  "nitpick" :: diag and
+  "nitpick_params" :: thy_decl
 begin
 
 typedecl bisim_iterator
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -10,22 +10,21 @@
   type fp_sugar =
     {T: typ,
      fp: BNF_FP_Util.fp_kind,
-     index: int,
-     pre_bnfs: BNF_Def.bnf list,
+     fp_res_index: int,
+     fp_res: BNF_FP_Util.fp_result,
+     pre_bnf: BNF_Def.bnf,
      nested_bnfs: BNF_Def.bnf list,
      nesting_bnfs: BNF_Def.bnf list,
-     fp_res: BNF_FP_Util.fp_result,
-     ctr_defss: thm list list,
-     ctr_sugars: Ctr_Sugar.ctr_sugar list,
-     co_iterss: term list list,
-     mapss: thm list list,
+     ctr_defs: thm list,
+     ctr_sugar: Ctr_Sugar.ctr_sugar,
+     co_iters: term list,
+     maps: thm list,
+     common_co_inducts: thm list,
      co_inducts: thm list,
-     co_inductss: thm list list,
-     co_iter_thmsss: thm list list list,
-     disc_co_itersss: thm list list list,
-     sel_co_iterssss: thm list list list list};
+     co_iter_thmss: thm list list,
+     disc_co_iterss: thm list list,
+     sel_co_itersss: thm list list list};
 
-  val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
   val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
   val fp_sugar_of: Proof.context -> string -> fp_sugar option
@@ -122,38 +121,40 @@
 type fp_sugar =
   {T: typ,
    fp: fp_kind,
-   index: int,
-   pre_bnfs: bnf list,
+   fp_res_index: int,
+   fp_res: fp_result,
+   pre_bnf: bnf,
    nested_bnfs: bnf list,
    nesting_bnfs: bnf list,
-   fp_res: fp_result,
-   ctr_defss: thm list list,
-   ctr_sugars: ctr_sugar list,
-   co_iterss: term list list,
-   mapss: thm list list,
+   ctr_defs: thm list,
+   ctr_sugar: Ctr_Sugar.ctr_sugar,
+   co_iters: term list,
+   maps: thm list,
+   common_co_inducts: thm list,
    co_inducts: thm list,
-   co_inductss: thm list list,
-   co_iter_thmsss: thm list list list,
-   disc_co_itersss: thm list list list,
-   sel_co_iterssss: thm list list list list};
-
-fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
+   co_iter_thmss: thm list list,
+   disc_co_iterss: thm list list,
+   sel_co_itersss: thm list list list};
 
-fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
-    ctr_sugars, co_iterss, mapss, co_inducts, co_inductss, co_iter_thmsss, disc_co_itersss,
-    sel_co_iterssss} : fp_sugar) =
-  {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
-    nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs,
+    ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss,
+    sel_co_itersss} : fp_sugar) =
+  {T = Morphism.typ phi T,
+   fp = fp,
    fp_res = morph_fp_result phi fp_res,
-   ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
-   ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
-   co_iterss = map (map (Morphism.term phi)) co_iterss,
-   mapss = map (map (Morphism.thm phi)) mapss,
+   fp_res_index = fp_res_index,
+   pre_bnf = morph_bnf phi pre_bnf,
+   nested_bnfs = map (morph_bnf phi) nested_bnfs,
+   nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+   ctr_defs = map (Morphism.thm phi) ctr_defs,
+   ctr_sugar = morph_ctr_sugar phi ctr_sugar,
+   co_iters = map (Morphism.term phi) co_iters,
+   maps = map (Morphism.thm phi) maps,
+   common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    co_inducts = map (Morphism.thm phi) co_inducts,
-   co_inductss = map (map (Morphism.thm phi)) co_inductss,
-   co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
-   disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
-   sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
+   co_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss,
+   disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss,
+   sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss};
 
 val transfer_fp_sugar =
   morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -183,15 +184,16 @@
     (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
-    ctr_sugars co_iterss mapss co_inducts co_inductss co_iter_thmsss disc_co_itersss
+    ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss
     sel_co_iterssss lthy =
   (0, lthy)
   |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
-    register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
-        nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
-        ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
-        co_inductss = co_inductss, co_iter_thmsss = co_iter_thmsss,
-        disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss}
+    register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk,
+        pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
+        ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk,
+        maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
+        co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
+        sel_co_itersss = nth sel_co_iterssss kk}
       lthy)) Ts
   |> snd;
 
@@ -1407,8 +1409,8 @@
         |> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
-          iterss mapss [induct_thm] (transpose [induct_thms]) (transpose [fold_thmss, rec_thmss])
-          [] []
+          iterss mapss [induct_thm] (map single induct_thms) (transpose [fold_thmss, rec_thmss])
+          (replicate nn []) (replicate nn [])
       end;
 
     fun derive_note_coinduct_coiters_thms_for_types
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -47,7 +47,8 @@
 
 fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
   let
-    fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
+    fun steal_fp_res get =
+      map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
 
     val n = length bnfs;
     val deads = fold (union (op =)) Dss resDs;
@@ -77,8 +78,8 @@
 
     val ((ctors, dtors), (xtor's, xtors)) =
       let
-        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
-        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
+        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal_fp_res #ctors);
+        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal_fp_res #dtors);
       in
         ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
       end;
@@ -92,9 +93,8 @@
       ||>> mk_Frees "x" xTs
       ||>> mk_Frees "y" yTs;
 
-    val fp_bnfs = steal #bnfs;
-    val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
-    val pre_bnfss = map #pre_bnfs fp_sugars;
+    val fp_bnfs = steal_fp_res #bnfs;
+    val pre_bnfs = map #pre_bnf fp_sugars;
     val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
     val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
     val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
@@ -126,9 +126,9 @@
 
     val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
 
-    val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
-    val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
-      |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
+    val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
+    val rel_xtor_co_inducts = steal_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
+      |> map (unfold_thms lthy (id_apply :: rel_unfolds));
 
     val rel_defs = map rel_def_of_bnf bnfs;
     val rel_monos = map rel_mono_of_bnf bnfs;
@@ -185,11 +185,13 @@
       |> mk_Frees' "s" fold_strTs
       ||>> mk_Frees' "s" rec_strTs;
 
-    val co_iters = steal #xtor_co_iterss;
-    val ns = map (length o #pre_bnfs) fp_sugars;
+    val co_iters = steal_fp_res #xtor_co_iterss;
+    val ns = map (length o #Ts o #fp_res) fp_sugars;
+
     fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
       | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
       | substT _ T = T;
+
     fun force_iter is_rec i TU TU_rec raw_iters =
       let
         val approx_fold = un_fold_of raw_iters
@@ -325,14 +327,14 @@
         val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
         val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
 
-        val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
-        val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
+        val map_unfolds = maps (fn bnf => no_refl [map_def_of_bnf bnf]) pre_bnfs;
+        val unfold_map = map (unfold_thms lthy (id_apply :: map_unfolds));
 
-        val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
+        val fp_xtor_co_iterss = steal_fp_res #xtor_co_iter_thmss;
         val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
         val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
 
-        val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
+        val fp_co_iter_o_mapss = steal_fp_res #xtor_co_iter_o_map_thmss;
         val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
         val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
         val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
@@ -358,20 +360,21 @@
        used by "primrec", "primcorecursive", and "datatype_compat". *)
     val fp_res =
       ({Ts = fpTs,
-        bnfs = steal #bnfs,
+        bnfs = steal_fp_res #bnfs,
         dtors = dtors,
         ctors = ctors,
         xtor_co_iterss = transpose [un_folds, co_recs],
         xtor_co_induct = xtor_co_induct_thm,
-        dtor_ctors = steal #dtor_ctors (*too general types*),
-        ctor_dtors = steal #ctor_dtors (*too general types*),
-        ctor_injects = steal #ctor_injects (*too general types*),
-        dtor_injects = steal #dtor_injects (*too general types*),
-        xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
-        xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
-        xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
+        dtor_ctors = steal_fp_res #dtor_ctors (*too general types*),
+        ctor_dtors = steal_fp_res #ctor_dtors (*too general types*),
+        ctor_injects = steal_fp_res #ctor_injects (*too general types*),
+        dtor_injects = steal_fp_res #dtor_injects (*too general types*),
+        xtor_map_thms = steal_fp_res #xtor_map_thms (*too general types and terms*),
+        xtor_set_thmss = steal_fp_res #xtor_set_thmss (*too general types and terms*),
+        xtor_rel_thms = steal_fp_res #xtor_rel_thms (*too general types and terms*),
         xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
-        xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
+        xtor_co_iter_o_map_thmss = steal_fp_res #xtor_co_iter_o_map_thmss
+          (*theorem about old constant*),
         rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
        |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   in
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -119,17 +119,18 @@
     val fp_b_names = map base_name_of_typ fpTs;
 
     val nn = length fpTs;
+    val kks = 0 upto nn - 1;
 
-    fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
+    fun target_ctr_sugar_of_fp_sugar fpT ({T, ctr_sugar, ...} : fp_sugar) =
       let
         val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
         val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
       in
-        morph_ctr_sugar phi (nth ctr_sugars index)
+        morph_ctr_sugar phi ctr_sugar
       end;
 
-    val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
-    val mapss = map (of_fp_sugar #mapss) fp_sugars0;
+    val ctr_defss = map #ctr_defs fp_sugars0;
+    val mapss = map #maps fp_sugars0;
     val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
 
     val ctrss = map #ctrs ctr_sugars;
@@ -215,14 +216,15 @@
               (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
           |>> split_list;
 
-        val ((co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
+        val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
               disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
           if fp = Least_FP then
             derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
               xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
               co_iterss co_iter_defss lthy
             |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
-              ([induct], [inducts], fold_thmss, rec_thmss, [], [], [], []))
+              ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [],
+               replicate nn [], replicate nn [], replicate nn []))
             ||> (fn info => (SOME info, NONE))
           else
             derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
@@ -232,32 +234,38 @@
             |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
                     (disc_unfold_thmss, disc_corec_thmss, _), _,
                     (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
-              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, corec_thmss,
-               disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
+              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss,
+               corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss,
+               sel_corec_thmsss))
             ||> (fn info => (NONE, SOME info));
 
         val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
-        fun mk_target_fp_sugar (kk, T) =
-          {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
-           nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
-           ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
-           co_inductss = transpose co_inductss,
-           co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
-           disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
-           sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
+        fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms
+            co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss =
+          {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
+           nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs,
+           ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
+           common_co_inducts = common_co_inducts, co_inducts = co_inducts,
+           co_iter_thmss = [un_fold_thms, co_rec_thms],
+           disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
+           sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]}
           |> morph_fp_sugar phi;
 
-        val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
+        val target_fp_sugars =
+          map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss
+            (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss
+            sel_unfold_thmsss sel_corec_thmsss;
+
+        val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
       in
         (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
       end)
   end;
 
 (* TODO: needed? *)
-fun indexify_callsss fp_sugar callsss =
+fun indexify_callsss (fp_sugar as {ctr_sugar = {ctrs, ...}, ...} : fp_sugar) callsss =
   let
-    val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
     fun indexify_ctr ctr =
       (case AList.lookup Term.aconv_untyped callsss ctr of
         NONE => replicate (num_binder_types (fastype_of ctr)) []
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -23,7 +23,6 @@
 open BNF_Comp
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
-open BNF_GFP_Rec_Sugar
 open BNF_GFP_Util
 open BNF_GFP_Tactics
 
@@ -164,8 +163,8 @@
      HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys;
     val hrecTs = map fastype_of Zeros;
 
-    val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
-      As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
+    val ((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
+      Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
       self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')),
       (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy
       |> mk_Frees' "b" activeAs
@@ -173,7 +172,6 @@
       ||>> mk_Frees "b" activeAs
       ||>> mk_Frees "b" activeBs
       ||>> mk_Frees' "y" passiveAs
-      ||>> mk_Frees "A" ATs
       ||>> mk_Frees "B" BTs
       ||>> mk_Frees "B" BTs
       ||>> mk_Frees "B'" B'Ts
@@ -204,7 +202,7 @@
       ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) activeAs) ATs);
 
     val passive_UNIVs = map HOLogic.mk_UNIV passiveAs;
-    val passive_Id_ons = map mk_Id_on As;
+    val passive_eqs = map HOLogic.eq_const passiveAs;
     val active_UNIVs = map HOLogic.mk_UNIV activeAs;
     val sum_UNIVs = map HOLogic.mk_UNIV sumBsAs;
     val passive_ids = map HOLogic.id_const passiveAs;
@@ -298,16 +296,16 @@
     val coalg_bind = mk_internal_b (coN ^ algN) ;
     val coalg_def_bind = (Thm.def_binding coalg_bind, []);
 
-    (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in A1 .. Am B1 ... Bn)*)
+    (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in UNIV .. UNIV B1 ... Bn)*)
     val coalg_spec =
       let
-        val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
+        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
         fun mk_coalg_conjunct B s X z z' =
           mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X)));
 
         val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
+        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
       end;
 
     val ((coalg_free, (_, coalg_def_free)), (lthy, lthy_old)) =
@@ -317,44 +315,44 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val coalg = fst (Term.dest_Const (Morphism.term phi coalg_free));
-    val coalg_def = mk_unabs_def (live + n) (Morphism.thm phi coalg_def_free RS meta_eq_to_obj_eq);
-
-    fun mk_coalg As Bs ss =
+    val coalg_def = mk_unabs_def (2 * n) (Morphism.thm phi coalg_def_free RS meta_eq_to_obj_eq);
+
+    fun mk_coalg Bs ss =
       let
-        val args = As @ Bs @ ss;
+        val args = Bs @ ss;
         val Ts = map fastype_of args;
         val coalgT = Library.foldr (op -->) (Ts, HOLogic.boolT);
       in
         Term.list_comb (Const (coalg, coalgT), args)
       end;
 
-    val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
+    val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
 
     val coalg_in_thms = map (fn i =>
       coalg_def RS iffD1 RS mk_conjunctN n i RS bspec) ks
 
     val coalg_set_thmss =
       let
-        val coalg_prem = HOLogic.mk_Trueprop (mk_coalg As Bs ss);
+        val coalg_prem = HOLogic.mk_Trueprop (mk_coalg Bs ss);
         fun mk_prem x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B));
         fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
         val prems = map2 mk_prem zs Bs;
-        val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) (As @ Bs) sets)
+        val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
           ss zs setssAs;
         val goalss = map3 (fn x => fn prem => fn concls => map (fn concl =>
-          fold_rev Logic.all (x :: As @ Bs @ ss)
+          fold_rev Logic.all (x :: Bs @ ss)
             (Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
       in
         map (fn goals => map (fn goal => Goal.prove_sorry lthy [] [] goal
           (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
       end;
 
-    fun mk_tcoalg ATs BTs = mk_coalg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
+    fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);
 
     val tcoalg_thm =
       let
         val goal = fold_rev Logic.all ss
-          (HOLogic.mk_Trueprop (mk_tcoalg passiveAs activeAs ss))
+          (HOLogic.mk_Trueprop (mk_tcoalg activeAs ss))
       in
         Goal.prove_sorry lthy [] [] goal
           (K (stac coalg_def 1 THEN CONJ_WRAP
@@ -720,8 +718,8 @@
         fun mk_bis R s s' b1 b2 RF map1 map2 sets =
           list_all_free [b1, b2] (HOLogic.mk_imp
             (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
-            mk_Bex (mk_in (As @ Rs) sets (snd (dest_Free RF))) (Term.absfree (dest_Free RF)
-              (HOLogic.mk_conj
+            mk_Bex (mk_in (passive_UNIVs @ Rs) sets (snd (dest_Free RF)))
+              (Term.absfree (dest_Free RF) (HOLogic.mk_conj
                 (HOLogic.mk_eq (Term.list_comb (map1, fst_args) $ RF, s $ b1),
                 HOLogic.mk_eq (Term.list_comb (map2, snd_args) $ RF, s' $ b2))))));
 
@@ -729,7 +727,7 @@
           (bis_le, Library.foldr1 HOLogic.mk_conj
             (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss @ B's @ s's @ Rs) rhs
+        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ Rs) rhs
       end;
 
     val ((bis_free, (_, bis_def_free)), (lthy, lthy_old)) =
@@ -739,11 +737,11 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val bis = fst (Term.dest_Const (Morphism.term phi bis_free));
-    val bis_def = mk_unabs_def (m + 5 * n) (Morphism.thm phi bis_def_free RS meta_eq_to_obj_eq);
-
-    fun mk_bis As Bs1 ss1 Bs2 ss2 Rs =
+    val bis_def = mk_unabs_def (5 * n) (Morphism.thm phi bis_def_free RS meta_eq_to_obj_eq);
+
+    fun mk_bis Bs1 ss1 Bs2 ss2 Rs =
       let
-        val args = As @ Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
+        val args = Bs1 @ ss1 @ Bs2 @ ss2 @ Rs;
         val Ts = map fastype_of args;
         val bisT = Library.foldr (op -->) (Ts, HOLogic.boolT);
       in
@@ -753,11 +751,11 @@
     val bis_cong_thm =
       let
         val prems = map HOLogic.mk_Trueprop
-         (mk_bis As Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
-        val concl = HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs_copy);
+         (mk_bis Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
+        val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
+          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
             (Logic.list_implies (prems, concl)))
           (K ((hyp_subst_tac lthy THEN' atac) 1))
         |> Thm.close_derivation
@@ -768,38 +766,38 @@
         fun mk_conjunct R s s' b1 b2 rel =
           list_all_free [b1, b2] (HOLogic.mk_imp
             (HOLogic.mk_mem (HOLogic.mk_prod (b1, b2), R),
-            Term.list_comb (rel, map mk_in_rel (passive_Id_ons @ Rs)) $ (s $ b1) $ (s' $ b2)));
+            Term.list_comb (rel, passive_eqs @ map mk_in_rel Rs) $ (s $ b1) $ (s' $ b2)));
 
         val rhs = HOLogic.mk_conj
           (bis_le, Library.foldr1 HOLogic.mk_conj
             (map6 mk_conjunct Rs ss s's zs z's relsAsBs))
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
-            (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
+          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
+            (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs)))
           (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_mapss))
         |> Thm.close_derivation
       end;
 
     val bis_converse_thm =
       Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
+        (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
           (Logic.mk_implies
-            (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
-            HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
+            (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+            HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs)))))
         (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
       |> Thm.close_derivation;
 
     val bis_O_thm =
       let
         val prems =
-          [HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
-           HOLogic.mk_Trueprop (mk_bis As B's s's B''s s''s R's)];
+          [HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+           HOLogic.mk_Trueprop (mk_bis B's s's B''s s''s R's)];
         val concl =
-          HOLogic.mk_Trueprop (mk_bis As Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
+          HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
+          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
             (Logic.list_implies (prems, concl)))
           (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
         |> Thm.close_derivation
@@ -808,10 +806,10 @@
     val bis_Gr_thm =
       let
         val concl =
-          HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map2 mk_Gr Bs fs));
+          HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
+          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
             (Logic.list_implies ([coalg_prem, mor_prem], concl)))
           (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
             morE_thms coalg_in_thms)
@@ -829,12 +827,12 @@
       let
         val prem =
           HOLogic.mk_Trueprop (mk_Ball Idx
-            (Term.absfree idx' (mk_bis As Bs ss B's s's (map (fn R => R $ idx) Ris))));
+            (Term.absfree idx' (mk_bis Bs ss B's s's (map (fn R => R $ idx) Ris))));
         val concl =
-          HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's (map (mk_UNION Idx) Ris));
+          HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris));
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
+          (fold_rev Logic.all (Idx :: Bs @ ss @ B's @ s's @ Ris)
             (Logic.mk_implies (prem, concl)))
           (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
         |> Thm.close_derivation
@@ -842,9 +840,9 @@
 
     (* self-bisimulation *)
 
-    fun mk_sbis As Bs ss Rs = mk_bis As Bs ss Bs ss Rs;
-
-    val sbis_prem = HOLogic.mk_Trueprop (mk_sbis As Bs ss sRs);
+    fun mk_sbis Bs ss Rs = mk_bis Bs ss Bs ss Rs;
+
+    val sbis_prem = HOLogic.mk_Trueprop (mk_sbis Bs ss sRs);
 
     (* largest self-bisimulation *)
 
@@ -853,10 +851,10 @@
     val lsbis_def_bind = rpair [] o Thm.def_binding o lsbis_bind;
 
     val all_sbis = HOLogic.mk_Collect (fst Rtuple', snd Rtuple', list_exists_free sRs
-      (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis As Bs ss sRs)));
+      (HOLogic.mk_conj (HOLogic.mk_eq (Rtuple, HOLogic.mk_tuple sRs), mk_sbis Bs ss sRs)));
 
     fun lsbis_spec i =
-      fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss)
+      fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss)
         (mk_UNION all_sbis (Term.absfree Rtuple' (mk_nthN n Rtuple i)));
 
     val ((lsbis_frees, (_, lsbis_def_frees)), (lthy, lthy_old)) =
@@ -869,12 +867,12 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val lsbis_defs = map (fn def =>
-      mk_unabs_def (live + n) (Morphism.thm phi def RS meta_eq_to_obj_eq)) lsbis_def_frees;
+      mk_unabs_def (2 * n) (Morphism.thm phi def RS meta_eq_to_obj_eq)) lsbis_def_frees;
     val lsbiss = map (fst o Term.dest_Const o Morphism.term phi) lsbis_frees;
 
-    fun mk_lsbis As Bs ss i =
+    fun mk_lsbis Bs ss i =
       let
-        val args = As @ Bs @ ss;
+        val args = Bs @ ss;
         val Ts = map fastype_of args;
         val RT = mk_relT (`I (HOLogic.dest_setT (fastype_of (nth Bs (i - 1)))));
         val lsbisT = Library.foldr (op -->) (Ts, RT);
@@ -884,8 +882,8 @@
 
     val sbis_lsbis_thm =
       Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all (As @ Bs @ ss)
-          (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
+        (fold_rev Logic.all (Bs @ ss)
+          (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks))))
         (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
       |> Thm.close_derivation;
 
@@ -896,8 +894,8 @@
 
     val incl_lsbis_thms =
       let
-        fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis As Bs ss i));
-        val goals = map2 (fn i => fn R => fold_rev Logic.all (As @ Bs @ ss @ sRs)
+        fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
+        val goals = map2 (fn i => fn R => fold_rev Logic.all (Bs @ ss @ sRs)
           (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
       in
         map3 (fn goal => fn i => fn def => Goal.prove_sorry lthy [] [] goal
@@ -906,8 +904,8 @@
 
     val equiv_lsbis_thms =
       let
-        fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis As Bs ss i));
-        val goals = map2 (fn i => fn B => fold_rev Logic.all (As @ Bs @ ss)
+        fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
+        val goals = map2 (fn i => fn B => fold_rev Logic.all (Bs @ ss)
           (Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs;
       in
         map3 (fn goal => fn l_incl => fn incl_l =>
@@ -1034,7 +1032,7 @@
     val isNode_def_bind = rpair [] o Thm.def_binding o isNode_bind;
 
     val isNodeT =
-      Library.foldr (op -->) (map fastype_of (As @ [Kl, lab, kl]), HOLogic.boolT);
+      Library.foldr (op -->) (map fastype_of [Kl, lab, kl], HOLogic.boolT);
 
     val Succs = map3 (fn i => fn k => fn k' =>
       HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl)))
@@ -1042,12 +1040,12 @@
 
     fun isNode_spec sets x i =
       let
-        val (passive_sets, active_sets) = chop m (map (fn set => set $ x) sets);
+        val active_sets = drop m (map (fn set => set $ x) sets);
         val rhs = list_exists_free [x]
           (Library.foldr1 HOLogic.mk_conj (HOLogic.mk_eq (lab $ kl, mk_InN bdFTs x i) ::
-          map2 mk_leq passive_sets As @ map2 (curry HOLogic.mk_eq) active_sets Succs));
+          map2 (curry HOLogic.mk_eq) active_sets Succs));
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ [Kl, lab, kl]) rhs
+        fold_rev (Term.absfree o Term.dest_Free) [Kl, lab, kl] rhs
       end;
 
     val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
@@ -1061,11 +1059,11 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val isNode_defs = map (fn def =>
-      mk_unabs_def (m + 3) (Morphism.thm phi def RS meta_eq_to_obj_eq)) isNode_def_frees;
+      mk_unabs_def 3 (Morphism.thm phi def RS meta_eq_to_obj_eq)) isNode_def_frees;
     val isNodes = map (fst o Term.dest_Const o Morphism.term phi) isNode_frees;
 
-    fun mk_isNode As kl i =
-      Term.list_comb (Const (nth isNodes (i - 1), isNodeT), As @ [Kl, lab, kl]);
+    fun mk_isNode kl i =
+      Term.list_comb (Const (nth isNodes (i - 1), isNodeT), [Kl, lab, kl]);
 
     val isTree =
       let
@@ -1075,9 +1073,9 @@
 
         val tree = mk_Ball Kl (Term.absfree kl'
           (HOLogic.mk_conj
-            (Library.foldr1 HOLogic.mk_disj (map (mk_isNode As kl) ks),
+            (Library.foldr1 HOLogic.mk_disj (map (mk_isNode kl) ks),
             Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' =>
-              mk_Ball Succ (Term.absfree k' (mk_isNode As
+              mk_Ball Succ (Term.absfree k' (mk_isNode
                 (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i)))
             Succs ks kks kks'))));
 
@@ -1093,13 +1091,9 @@
     val carT_def_bind = rpair [] o Thm.def_binding o carT_bind;
 
     fun carT_spec i =
-      let
-        val rhs = HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
-          (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
-            HOLogic.mk_conj (isTree, mk_isNode As (HOLogic.mk_list sum_sbdT []) i))));
-      in
-        fold_rev (Term.absfree o Term.dest_Free) As rhs
-      end;
+      HOLogic.mk_Collect (fst Kl_lab', snd Kl_lab', list_exists_free [Kl, lab]
+        (HOLogic.mk_conj (HOLogic.mk_eq (Kl_lab, HOLogic.mk_prod (Kl, lab)),
+          HOLogic.mk_conj (isTree, mk_isNode (HOLogic.mk_list sum_sbdT []) i))));
 
     val ((carT_frees, (_, carT_def_frees)), (lthy, lthy_old)) =
       lthy
@@ -1110,13 +1104,10 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
-    val carT_defs = map (fn def =>
-      mk_unabs_def m (Morphism.thm phi def RS meta_eq_to_obj_eq)) carT_def_frees;
+    val carT_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) carT_def_frees;
     val carTs = map (fst o Term.dest_Const o Morphism.term phi) carT_frees;
 
-    fun mk_carT As i = Term.list_comb
-      (Const (nth carTs (i - 1),
-         Library.foldr (op -->) (map fastype_of As, HOLogic.mk_setT treeT)), As);
+    fun mk_carT i = Const (nth carTs (i - 1), HOLogic.mk_setT treeT);
 
     val strT_binds = mk_internal_bs strTN;
     fun strT_bind i = nth strT_binds (i - 1);
@@ -1153,12 +1144,11 @@
 
     fun mk_strT FT i = Const (nth strTs (i - 1), treeT --> FT);
 
-    val carTAs = map (mk_carT As) ks;
+    val carTAs = map mk_carT ks;
     val strTAs = map2 mk_strT treeFTs ks;
 
     val coalgT_thm =
-      Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
+      Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg carTAs strTAs))
         (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
           (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
       |> Thm.close_derivation;
@@ -1406,36 +1396,6 @@
         map (fn i => map (fn i' => rv_last' RS mk_conjunctN n i RS mk_conjunctN n i') ks) ks
       end;
 
-    val set_rv_Lev_thmsss = if m = 0 then replicate n (replicate n []) else
-      let
-        fun mk_case s sets z z_free = Term.absfree z_free (Library.foldr1 HOLogic.mk_conj
-          (map2 (fn set => fn A => mk_leq (set $ (s $ z)) A) (take m sets) As));
-
-        fun mk_conjunct i z B = HOLogic.mk_imp
-          (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), HOLogic.mk_mem (z, B)),
-          mk_case_sumN (map4 mk_case ss setssAs zs zs') $ (mk_rv ss kl i $ z));
-
-        val goal = list_all_free (kl :: zs)
-          (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct ks zs Bs));
-
-        val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
-
-        val set_rv_Lev = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] []
-            (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
-            (K (mk_set_rv_Lev_tac lthy m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
-              coalg_set_thmss from_to_sbd_thmss)))
-          |> Thm.close_derivation;
-
-        val set_rv_Lev' = mk_specN (n + 1) set_rv_Lev;
-      in
-        map (fn i => map (fn i' =>
-          split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
-            else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
-              (2, @{thm sum.weak_case_cong} RS iffD1) RS
-              (mk_sum_caseN n i' RS iffD1))) ks) ks
-      end;
-
     val set_Lev_thmsss =
       let
         fun mk_conjunct i z =
@@ -1515,29 +1475,25 @@
 
     val mor_beh_thm =
       Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all (As @ Bs @ ss) (Logic.mk_implies (coalg_prem,
-          HOLogic.mk_Trueprop (mk_mor Bs ss carTAs strTAs (map (mk_beh ss) ks)))))
+        (fold_rev Logic.all ss (HOLogic.mk_Trueprop
+          (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks))))
         (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
           beh_defs carT_defs strT_defs isNode_defs
           to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
-          length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
-          set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
-          set_mapss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
+          length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss set_Lev_thmsss
+          set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s map_arg_cong_thms)
       |> Thm.close_derivation;
 
     val timer = time (timer "Behavioral morphism");
 
-    fun mk_LSBIS As i = mk_lsbis As (map (mk_carT As) ks) strTAs i;
-    fun mk_car_final As i =
-      mk_quotient (mk_carT As i) (mk_LSBIS As i);
-    fun mk_str_final As i =
+    val lsbisAs = map (mk_lsbis carTAs strTAs) ks;
+
+    fun mk_str_final i =
       mk_univ (HOLogic.mk_comp (Term.list_comb (nth final_maps (i - 1),
-        passive_ids @ map (mk_proj o mk_LSBIS As) ks), nth strTAs (i - 1)));
-
-    val car_finalAs = map (mk_car_final As) ks;
-    val str_finalAs = map (mk_str_final As) ks;
-    val car_finals = map (mk_car_final passive_UNIVs) ks;
-    val str_finals = map (mk_str_final passive_UNIVs) ks;
+        passive_ids @ map mk_proj lsbisAs), nth strTAs (i - 1)));
+
+    val car_finals = map2 mk_quotient carTAs lsbisAs;
+    val str_finals = map mk_str_final ks;
 
     val coalgT_set_thmss = map (map (fn thm => coalgT_thm RS thm)) coalg_set_thmss;
     val equiv_LSBIS_thms = map (fn thm => coalgT_thm RS thm) equiv_lsbis_thms;
@@ -1545,11 +1501,10 @@
     val congruent_str_final_thms =
       let
         fun mk_goal R final_map strT =
-          fold_rev Logic.all As (HOLogic.mk_Trueprop
-            (mk_congruent R (HOLogic.mk_comp
-              (Term.list_comb (final_map, passive_ids @ map (mk_proj o mk_LSBIS As) ks), strT))));
-
-        val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs;
+          HOLogic.mk_Trueprop (mk_congruent R (HOLogic.mk_comp
+            (Term.list_comb (final_map, passive_ids @ map mk_proj lsbisAs), strT)));
+
+        val goals = map3 mk_goal lsbisAs final_maps strTAs;
       in
         map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
@@ -1558,21 +1513,19 @@
         goals lsbisE_thms map_comp_id_thms map_cong0s
       end;
 
-    val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
-      (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs)))
+    val coalg_final_thm = Goal.prove_sorry lthy [] []
+      (HOLogic.mk_Trueprop (mk_coalg car_finals str_finals))
       (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms
         set_mapss coalgT_set_thmss))
       |> Thm.close_derivation;
 
-    val mor_T_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
-      (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finalAs str_finalAs
-        (map (mk_proj o mk_LSBIS As) ks))))
+    val mor_T_final_thm = Goal.prove_sorry lthy [] []
+      (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs)))
       (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms))
       |> Thm.close_derivation;
 
     val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
-    val in_car_final_thms = map (fn mor_image' => mor_image' OF
-      [tcoalg_thm RS mor_final_thm, UNIV_I]) mor_image'_thms;
+    val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
 
     val timer = time (timer "Final coalgebra");
 
@@ -1661,7 +1614,7 @@
         val mor_Rep =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
-            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m (mor_def :: dtor_defs) Reps
+            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt (mor_def :: dtor_defs) Reps
               Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
           |> Thm.close_derivation;
 
@@ -1687,7 +1640,7 @@
       |> fold_map4 (fn i => fn abs => fn f => fn z =>
         Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
           ks Abs_Ts (map (fn i => HOLogic.mk_comp
-            (mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs
+            (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs
       |>> apsnd split_list o split_list
       ||> `Local_Theory.restore;
 
@@ -1707,8 +1660,7 @@
     val mor_unfold_thm =
       let
         val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
-        val morEs' = map (fn thm =>
-          (thm OF [tcoalg_thm RS mor_final_thm, UNIV_I]) RS sym) morE_thms;
+        val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all ss
@@ -1721,7 +1673,7 @@
 
     val (raw_coind_thms, raw_coind_thm) =
       let
-        val prem = HOLogic.mk_Trueprop (mk_sbis passive_UNIVs UNIVs dtors TRs);
+        val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs);
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
         val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
@@ -1741,7 +1693,7 @@
           (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 mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];
 
         val unique_mor = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
@@ -1926,7 +1878,7 @@
 
         fun mk_rel_prem phi dtor rel Jz Jz_copy =
           let
-            val concl = Term.list_comb (rel, map HOLogic.eq_const passiveAs @ phis) $
+            val concl = Term.list_comb (rel, passive_eqs @ phis) $
               (dtor $ Jz) $ (dtor $ Jz_copy);
           in
             HOLogic.mk_Trueprop
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2013
 
-Corecursor sugar.
+Corecursor sugar ("primcorec" and "primcorecursive").
 *)
 
 signature BNF_GFP_REC_SUGAR =
@@ -367,9 +367,7 @@
   | _ => not_codatatype ctxt res_T);
 
 fun map_thms_of_typ ctxt (Type (s, _)) =
-    (case fp_sugar_of ctxt s of
-      SOME {index, mapss, ...} => nth mapss index
-    | NONE => [])
+    (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
   | map_thms_of_typ _ _ = [];
 
 fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
@@ -378,15 +376,15 @@
 
     val ((missing_res_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
-            co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
+            common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
       nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0;
 
-    val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
+    val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
 
-    val indices = map #index fp_sugars;
-    val perm_indices = map #index perm_fp_sugars;
+    val indices = map #fp_res_index fp_sugars;
+    val perm_indices = map #fp_res_index perm_fp_sugars;
 
-    val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
+    val perm_ctrss = map (#ctrs o #ctr_sugar) perm_fp_sugars;
     val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
     val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss;
 
@@ -395,8 +393,8 @@
     val kks = 0 upto nn - 1;
     val perm_ns = map length perm_ctr_Tsss;
 
-    val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
-      of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
+    val perm_Cs = map (fn {fp_res, fp_res_index, ...} => domain_type (body_fun_type (fastype_of
+      (co_rec_of (nth (#xtor_co_iterss fp_res) fp_res_index))))) perm_fp_sugars;
     val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
       mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
 
@@ -410,7 +408,7 @@
     fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
     fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
 
-    val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
+    val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms;
 
     val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
     val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
@@ -444,35 +442,32 @@
          disc_corec = disc_corec, sel_corecs = sel_corecs}
       end;
 
-    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
-        sel_coiterssss =
+    fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
+        : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss =
       let
-        val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar =
-          nth ctr_sugars index;
         val p_ios = map SOME p_is @ [NONE];
-        val discIs = #discIs (nth ctr_sugars index);
-        val corec_thms = co_rec_of (nth coiter_thmsss index);
-        val disc_corecs = co_rec_of (nth disc_coitersss index);
-        val sel_corecss = co_rec_of (nth sel_coiterssss index);
+        val corec_thms = co_rec_of coiter_thmss;
+        val disc_corecs = co_rec_of disc_coiterss;
+        val sel_corecss = co_rec_of sel_coitersss;
       in
         map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
           disc_excludesss collapses corec_thms disc_corecs sel_corecss
       end;
 
-    fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
-          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
-        p_is q_isss f_isss f_Tsss =
-      {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
-       disc_exhausts = #disc_exhausts (nth ctr_sugars index),
+    fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters,
+        co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss,
+        sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+      {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters),
+       disc_exhausts = disc_exhausts,
        nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
        nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
        nested_map_comps = map map_comp_of_bnf nested_bnfs,
-       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
-         disc_coitersss sel_coiterssss};
+       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss
+         sel_coitersss};
   in
     ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
-      co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
-      strong_co_induct_of coinduct_thmss), lthy)
+      co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
+      co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss), lthy)
   end;
 
 val undef_const = Const (@{const_name undefined}, dummyT);
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -48,15 +48,14 @@
   val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
   val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
   val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
-  val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list list ->
+  val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
     thm list -> thm list -> tactic
   val mk_mor_T_final_tac: thm -> thm list -> thm list -> tactic
   val mk_mor_UNIV_tac: thm list -> thm -> tactic
   val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list ->
     thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list ->
     thm list -> 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 -> tactic
+    thm list list list -> thm list list -> thm list -> thm list -> thm list -> tactic
   val mk_mor_case_sum_tac: 'a list -> thm -> tactic
   val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
   val mk_mor_elim_tac: thm -> tactic
@@ -87,8 +86,6 @@
   val mk_set_ge_tac: int  -> thm -> thm list -> tactic
   val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
   val mk_set_map0_tac: thm -> thm -> tactic
-  val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
-    thm list -> thm list -> thm list list -> thm list list -> tactic
   val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic
@@ -108,8 +105,6 @@
 val nat_induct = @{thm nat_induct};
 val o_apply_trans_sym = o_apply RS trans RS sym;
 val ord_eq_le_trans = @{thm ord_eq_le_trans};
-val ord_eq_le_trans_trans_fun_cong_image_id_id_apply =
-  @{thm ord_eq_le_trans[OF trans[OF fun_cong[OF image_id] id_apply]]};
 val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
 val sum_weak_case_cong = @{thm sum.weak_case_cong};
@@ -117,10 +112,6 @@
 val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
 val rev_bspec = Drule.rotate_prems 1 bspec;
 val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
-val conversep_in_rel_Id_on =
-   @{thm trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]};
-val relcompp_in_rel_Id_on =
-   @{thm   trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]};
 val converse_shift = @{thm converse_subset_swap} RS iffD1;
 
 fun mk_coalg_set_tac coalg_def =
@@ -245,8 +236,8 @@
             CONJ_WRAP' (fn (i, thm) =>
               if i <= m
               then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
-                etac @{thm image_mono}, rtac @{thm image_subsetI},
-                etac @{thm Collect_split_in_relI[OF Id_onI]}]
+                etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI,
+                rtac @{thm case_prodI}, rtac refl]
               else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
                 rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
             (1 upto (m + n) ~~ set_map0s)])
@@ -266,13 +257,11 @@
         REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
         REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
         rtac trans, rtac map_cong0,
-        REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
+        REPEAT_DETERM_N m o EVERY' [rtac @{thm Collect_splitD}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,
         atac, rtac CollectI,
         CONJ_WRAP' (fn (i, thm) =>
-          if i <= m
-          then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
-            rtac @{thm Id_on_fst}, etac set_mp, atac]
+          if i <= m then rtac subset_UNIV
           else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
             rtac trans_fun_cong_image_id_id_apply, atac])
         (1 upto (m + n) ~~ set_map0s)];
@@ -290,7 +279,7 @@
     CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
       EVERY' [rtac allI, rtac allI, rtac impI,
         rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
-        REPEAT_DETERM_N m o rtac conversep_in_rel_Id_on,
+        REPEAT_DETERM_N m o rtac @{thm conversep_eq},
         REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
         rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
         REPEAT_DETERM o etac allE,
@@ -303,7 +292,7 @@
     CONJ_WRAP' (fn (rel_cong, rel_OO) =>
       EVERY' [rtac allI, rtac allI, rtac impI,
         rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
-        REPEAT_DETERM_N m o rtac relcompp_in_rel_Id_on,
+        REPEAT_DETERM_N m o rtac @{thm eq_OO},
         REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
         rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
         etac @{thm relcompE},
@@ -313,7 +302,7 @@
         etac mp, atac, etac mp, atac]) (rel_congs ~~ rel_OOs)] 1;
 
 fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
-  unfold_thms_tac ctxt (bis_rel :: @{thm Id_on_Gr} :: @{thm in_rel_Gr} :: rel_Grps) THEN
+  unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) 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) =>
@@ -373,13 +362,11 @@
   let
     val n = length strT_defs;
     val ks = 1 upto n;
-    fun coalg_tac (i, ((passive_sets, active_sets), def)) =
+    fun coalg_tac (i, (active_sets, def)) =
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
         hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
         rtac (mk_sum_caseN n i), rtac CollectI,
-        EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
-          etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
-          passive_sets),
+        REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
         CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
           rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
           rtac conjI,
@@ -397,7 +384,6 @@
               REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI,
               rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans),
               rtac (@{thm append_Cons} RS sym RS arg_cong RS trans), atac,
-              REPEAT_DETERM_N m o (rtac conjI THEN' atac),
               CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong},
                 rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
                 rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks,
@@ -414,7 +400,7 @@
             rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
   in
     unfold_thms_tac ctxt defs THEN
-    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_map0ss ~~ strT_defs)) 1
+    CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1
   end;
 
 fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
@@ -519,35 +505,6 @@
       ks)] 1
   end;
 
-fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
-  let
-    val n = length Lev_0s;
-    val ks = 1 upto n;
-  in
-    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
-      REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn (i, ((Lev_0, rv_Nil), coalg_sets)) =>
-        EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
-          dtac (Lev_0 RS equalityD1 RS set_mp), etac @{thm singletonE}, etac ssubst,
-          rtac (rv_Nil RS arg_cong RS iffD2),
-          rtac (mk_sum_caseN n i RS iffD2),
-          CONJ_WRAP' (fn thm => etac thm THEN' atac) (take m coalg_sets)])
-      (ks ~~ ((Lev_0s ~~ rv_Nils) ~~ coalg_setss)),
-      REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn ((Lev_Suc, rv_Cons), (from_to_sbds, coalg_sets)) =>
-        EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
-          CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
-            (fn (i, (from_to_sbd, coalg_set)) =>
-              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
-              rtac (rv_Cons RS arg_cong RS iffD2),
-              rtac (mk_sum_caseN n i RS arg_cong RS trans RS iffD2),
-              etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
-              dtac (mk_conjunctN n i), etac mp, etac conjI, etac set_rev_mp,
-              etac coalg_set, atac])
-          (rev (ks ~~ (from_to_sbds ~~ drop m coalg_sets)))])
-      ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
-  end;
-
 fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
   let
     val n = length Lev_0s;
@@ -655,7 +612,7 @@
 
 fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
-  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss
+  prefCl_Levs rv_lastss set_Levsss set_image_Levsss set_map0ss
   map_comp_ids map_cong0s map_arg_congs =
   let
     val n = length beh_defs;
@@ -663,7 +620,7 @@
 
     fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
       ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s,
-        (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
+        (set_Levss, set_image_Levss))))))))))) =
       EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
         rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
         rtac conjI,
@@ -678,18 +635,12 @@
         rtac conjI,
           rtac ballI, etac @{thm UN_E}, rtac conjI,
           if n = 1 then K all_tac else rtac (mk_sumEN n),
-          EVERY' (map6 (fn i => fn isNode_def => fn set_map0s =>
-            fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
+          EVERY' (map5 (fn i => fn isNode_def => fn set_map0s => fn set_Levs => fn set_image_Levs =>
             EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
               rtac exI, rtac conjI,
               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
               else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
                 etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
-              EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
-                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
-                  rtac trans_fun_cong_image_id_id_apply,
-                  etac set_rv_Lev, TRY o atac, etac conjI, atac])
-              (take m set_map0s) set_rv_Levs),
               CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
                 EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -699,9 +650,9 @@
                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
                   if n = 1 then rtac refl else atac])
               (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
-          ks isNode_defs set_map0ss set_rv_Levss set_Levss set_image_Levss),
+          ks isNode_defs set_map0ss set_Levss set_image_Levss),
           CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
-            (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
+            (set_Levs, set_image_Levs))))) =>
             EVERY' [rtac ballI,
               REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
               rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
@@ -709,11 +660,6 @@
               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
               else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
                 etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)),
-              EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
-                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
-                  rtac trans_fun_cong_image_id_id_apply,
-                  etac set_rv_Lev, TRY o atac, etac conjI, atac])
-              (take m set_map0s) set_rv_Levs),
               CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
                 EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
@@ -726,7 +672,7 @@
                   if n = 1 then rtac refl else atac])
               (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
           (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
-            (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
+            (set_Levss ~~ set_image_Levss))))),
         (**)
           rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
           etac notE, etac @{thm UN_I[OF UNIV_I]},
@@ -736,10 +682,6 @@
           CONVERSION (Conv.top_conv
             (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
           if n = 1 then rtac refl else rtac (mk_sum_caseN n i),
-          EVERY' (map2 (fn set_map0 => fn coalg_set =>
-            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
-              rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
-            (take m set_map0s) (take m coalg_sets)),
           CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
             EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
               rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
@@ -768,7 +710,7 @@
         EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
           DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
-            rtac equalityI, rtac subsetI, etac thin_rl, etac thin_rl,
+            rtac equalityI, rtac subsetI, etac thin_rl, 
             REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
             etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},
             rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc,
@@ -811,8 +753,7 @@
     CONJ_WRAP' fbetw_tac
       (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
         ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
-          (set_map0ss ~~ (coalg_setss ~~
-            (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
+          (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))))) THEN'
     CONJ_WRAP' mor_tac
       (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
         ((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
@@ -834,16 +775,12 @@
     CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
       EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
         rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
-        EVERY' (map2 (fn set_map0 => fn coalgT_set =>
-          EVERY' [rtac conjI, rtac (set_map0 RS ord_eq_le_trans),
-            rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
-            etac coalgT_set])
-        (take m set_map0s) (take m coalgT_sets)),
+        REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
         CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
           EVERY' [rtac (set_map0 RS ord_eq_le_trans),
             rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
             rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
-        (equiv_LSBISs ~~ drop m (set_map0s ~~ coalgT_sets))])
+        (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))])
     ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
 
 fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
@@ -856,7 +793,7 @@
         rtac congruent_str_final, atac, rtac o_apply])
     (equiv_LSBISs ~~ congruent_str_finals)] 1;
 
-fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
+fun mk_mor_Rep_tac ctxt defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls =
   unfold_thms_tac ctxt defs THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
@@ -865,7 +802,7 @@
         EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
           EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
             etac set_rev_mp, rtac coalg_final_set, rtac Rep])
-        Abs_inverses (drop m coalg_final_sets))])
+        Abs_inverses coalg_final_sets)])
     (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
 
 fun mk_mor_Abs_tac ctxt defs Abs_inverses =
@@ -940,7 +877,7 @@
     rel_congs,
     CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,
       REPEAT_DETERM o etac allE, rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
-      REPEAT_DETERM_N m o rtac @{thm in_rel_Id_on_UNIV[symmetric]},
+      REPEAT_DETERM_N m o rtac refl,
       REPEAT_DETERM_N (length rel_congs) o rtac @{thm in_rel_Collect_split_eq[symmetric]},
       etac mp, etac CollectE, etac @{thm splitD}])
     rel_congs,
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -22,7 +22,6 @@
 open BNF_Comp
 open BNF_FP_Util
 open BNF_FP_Def_Sugar
-open BNF_LFP_Rec_Sugar
 open BNF_LFP_Util
 open BNF_LFP_Tactics
 
@@ -86,7 +85,6 @@
     val FTsAs = mk_FTs allAs;
     val FTsBs = mk_FTs allBs;
     val FTsCs = mk_FTs allCs;
-    val ATs = map HOLogic.mk_setT passiveAs;
     val BTs = map HOLogic.mk_setT activeAs;
     val B'Ts = map HOLogic.mk_setT activeBs;
     val B''Ts = map HOLogic.mk_setT activeCs;
@@ -121,11 +119,10 @@
       bd0s Dss bnfs;
     val witss = map wits_of_bnf bnfs;
 
-    val (((((((((((((((((((zs, zs'), As), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
+    val ((((((((((((((((((zs, zs'), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s),
       fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')), (yFs, yFs')),
       names_lthy) = lthy
       |> mk_Frees' "z" activeAs
-      ||>> mk_Frees "A" ATs
       ||>> mk_Frees "B" BTs
       ||>> mk_Frees "B" BTs
       ||>> mk_Frees "B'" B'Ts
@@ -246,16 +243,16 @@
     val alg_bind = mk_internal_b algN;
     val alg_def_bind = (Thm.def_binding alg_bind, []);
 
-    (*forall i = 1 ... n: (\<forall>x \<in> Fi_in A1 .. Am B1 ... Bn. si x \<in> Bi)*)
+    (*forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV .. UNIV B1 ... Bn. si x \<in> Bi)*)
     val alg_spec =
       let
-        val ins = map3 mk_in (replicate n (As @ Bs)) setssAs FTsAs;
+        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
         fun mk_alg_conjunct B s X x x' =
           mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
 
         val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ Bs @ ss) rhs
+        fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
       end;
 
     val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
@@ -265,11 +262,11 @@
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
-    val alg_def = mk_unabs_def (live + n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
+    val alg_def = mk_unabs_def (2 * n) (Morphism.thm phi alg_def_free RS meta_eq_to_obj_eq);
 
-    fun mk_alg As Bs ss =
+    fun mk_alg Bs ss =
       let
-        val args = As @ Bs @ ss;
+        val args = Bs @ ss;
         val Ts = map fastype_of args;
         val algT = Library.foldr (op -->) (Ts, HOLogic.boolT);
       in
@@ -278,13 +275,13 @@
 
     val alg_set_thms =
       let
-        val alg_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+        val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
         fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
-        val premss = map2 ((fn x => fn sets =>  map2 (mk_prem x) sets (As @ Bs))) xFs setssAs;
+        val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
         val concls = map3 mk_concl ss xFs Bs;
         val goals = map3 (fn x => fn prems => fn concl =>
-          fold_rev Logic.all (x :: As @ Bs @ ss)
+          fold_rev Logic.all (x :: Bs @ ss)
             (Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
       in
         map (fn goal =>
@@ -292,12 +289,12 @@
         goals
       end;
 
-    fun mk_talg ATs BTs = mk_alg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
+    fun mk_talg BTs = mk_alg (map HOLogic.mk_UNIV BTs);
 
     val talg_thm =
       let
         val goal = fold_rev Logic.all ss
-          (HOLogic.mk_Trueprop (mk_talg passiveAs activeAs ss))
+          (HOLogic.mk_Trueprop (mk_talg activeAs ss))
       in
         Goal.prove_sorry lthy [] [] goal
           (K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
@@ -309,7 +306,7 @@
     val alg_not_empty_thms =
       let
         val alg_prem =
-          HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+          HOLogic.mk_Trueprop (mk_alg Bs ss);
         val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs;
         val goals =
           map (fn concl =>
@@ -416,9 +413,7 @@
         fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
           HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
         val prems = map HOLogic.mk_Trueprop
-          ([mk_mor Bs ss B's s's fs,
-          mk_alg passive_UNIVs Bs ss,
-          mk_alg passive_UNIVs B's s's] @
+          ([mk_mor Bs ss B's s's fs, mk_alg Bs ss, mk_alg B's s's] @
           map4 mk_inv_prem fs inv_fs Bs B's);
         val concl = HOLogic.mk_Trueprop (mk_mor B's s's Bs ss inv_fs);
       in
@@ -498,9 +493,7 @@
 
     val iso_alt_thm =
       let
-        val prems = map HOLogic.mk_Trueprop
-         [mk_alg passive_UNIVs Bs ss,
-         mk_alg passive_UNIVs B's s's]
+        val prems = map HOLogic.mk_Trueprop [mk_alg Bs ss, mk_alg B's s's]
         val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
           HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
             Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
@@ -518,7 +511,7 @@
     val (copy_alg_thm, ex_copy_alg_thm) =
       let
         val prems = map HOLogic.mk_Trueprop
-         (mk_alg passive_UNIVs Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
+         (mk_alg Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
         val inver_prems = map HOLogic.mk_Trueprop
           (map3 mk_inver inv_fs fs Bs @ map3 mk_inver fs inv_fs B's);
         val all_prems = prems @ inver_prems;
@@ -526,7 +519,7 @@
           (Term.list_comb (mapT, passive_ids @ inv_fs) $ y)));
 
         val alg = HOLogic.mk_Trueprop
-          (mk_alg passive_UNIVs B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
+          (mk_alg B's (map5 mk_s fs ss mapsBsAs yFs yFs'));
         val copy_str_thm = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
             (Logic.list_implies (all_prems, alg)))
@@ -543,7 +536,7 @@
 
         val ex = HOLogic.mk_Trueprop
           (list_exists_free s's
-            (HOLogic.mk_conj (mk_alg passive_UNIVs B's s's,
+            (HOLogic.mk_conj (mk_alg B's s's,
               mk_iso B's s's Bs ss inv_fs fs_copy)));
         val ex_copy_alg_thm = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
@@ -594,7 +587,9 @@
     val suc_bd_Asuc_bd = @{thm ordLess_ordLeq_trans[OF ordLess_ctwo_cexp cexp_mono1]} OF
       [suc_bd_Card_order, basis_Asuc, suc_bd_Card_order];
 
-    val Asuc_bdT = fst (dest_relT (fastype_of (mk_Asuc_bd As)));
+
+    val Asuc_bd = mk_Asuc_bd passive_UNIVs;
+    val Asuc_bdT = fst (dest_relT (fastype_of Asuc_bd));
     val II_BTs = replicate n (HOLogic.mk_setT Asuc_bdT);
     val II_sTs = map2 (fn Ds => fn bnf =>
       mk_T_of_bnf Ds (passiveAs @ replicate n Asuc_bdT) bnf --> Asuc_bdT) Dss bnfs;
@@ -632,31 +627,31 @@
     fun mk_minG Asi i k = mk_UNION (mk_underS suc_bd $ i)
       (Term.absfree jdx' (mk_nthN n (Asi $ jdx) k));
 
-    fun mk_minH_component As Asi i sets Ts s k =
+    fun mk_minH_component Asi i sets Ts s k =
       HOLogic.mk_binop @{const_name "sup"}
-      (mk_minG Asi i k, mk_image s $ mk_in (As @ map (mk_minG Asi i) ks) sets Ts);
+      (mk_minG Asi i k, mk_image s $ mk_in (passive_UNIVs @ map (mk_minG Asi i) ks) sets Ts);
 
-    fun mk_min_algs As ss =
+    fun mk_min_algs ss =
       let
         val BTs = map (range_type o fastype_of) ss;
-        val Ts = map (HOLogic.dest_setT o fastype_of) As @ BTs;
+        val Ts = passiveAs @ BTs;
         val (Asi, Asi') = `Free (Asi_name, suc_bdT -->
           Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs));
       in
          mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple
-           (map4 (mk_minH_component As Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
+           (map4 (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
       end;
 
     val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) =
       let
         val i_field = HOLogic.mk_mem (idx, field_suc_bd);
-        val min_algs = mk_min_algs As ss;
+        val min_algs = mk_min_algs ss;
         val min_algss = map (fn k => mk_nthN n (min_algs $ idx) k) ks;
 
         val concl = HOLogic.mk_Trueprop
           (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
-            (map4 (mk_minH_component As min_algs idx) setssAs FTsAs ss ks)));
-        val goal = fold_rev Logic.all (idx :: As @ ss)
+            (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
+        val goal = fold_rev Logic.all (idx :: ss)
           (Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
 
         val min_algs_thm = Goal.prove_sorry lthy [] [] goal
@@ -666,7 +661,7 @@
         val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
 
         fun mk_mono_goal min_alg =
-          fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_relChain suc_bd
+          fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_relChain suc_bd
             (Term.absfree idx' min_alg)));
 
         val monos =
@@ -675,8 +670,6 @@
             |> Thm.close_derivation)
           (map mk_mono_goal min_algss) min_algs_thms;
 
-        val Asuc_bd = mk_Asuc_bd As;
-
         fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
         val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
         val card_cT = certifyT lthy suc_bdT;
@@ -691,7 +684,7 @@
               suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
           |> Thm.close_derivation;
 
-        val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+        val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
         val least_cT = certifyT lthy suc_bdT;
         val least_ct = certify lthy (Term.absfree idx' least_conjunction);
@@ -716,9 +709,9 @@
     fun min_alg_spec i =
       let
         val rhs = mk_UNION (field_suc_bd)
-          (Term.absfree idx' (mk_nthN n (mk_min_algs As ss $ idx) i));
+          (Term.absfree idx' (mk_nthN n (mk_min_algs ss $ idx) i));
       in
-        fold_rev (Term.absfree o Term.dest_Free) (As @ ss) rhs
+        fold_rev (Term.absfree o Term.dest_Free) ss rhs
       end;
 
     val ((min_alg_frees, (_, min_alg_def_frees)), (lthy, lthy_old)) =
@@ -731,47 +724,45 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val min_algs = map (fst o Term.dest_Const o Morphism.term phi) min_alg_frees;
     val min_alg_defs = map (fn def =>
-      mk_unabs_def live (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
+      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) min_alg_def_frees;
 
-    fun mk_min_alg As ss i =
+    fun mk_min_alg ss i =
       let
         val T = HOLogic.mk_setT (range_type (fastype_of (nth ss (i - 1))))
-        val args = As @ ss;
-        val Ts = map fastype_of args;
+        val Ts = map fastype_of ss;
         val min_algT = Library.foldr (op -->) (Ts, T);
       in
-        Term.list_comb (Const (nth min_algs (i - 1), min_algT), args)
+        Term.list_comb (Const (nth min_algs (i - 1), min_algT), ss)
       end;
 
     val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
       let
-        val min_algs = map (mk_min_alg As ss) ks;
+        val min_algs = map (mk_min_alg ss) ks;
 
-        val goal = fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_alg As min_algs ss));
+        val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
         val alg_min_alg = Goal.prove_sorry lthy [] [] goal
           (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite
             set_bd_sumss min_algs_thms min_algs_mono_thms))
           |> Thm.close_derivation;
 
-        val Asuc_bd = mk_Asuc_bd As;
         fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ ss)
+          (fold_rev Logic.all ss
             (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
           (K (mk_card_of_min_alg_tac def card_of_min_algs_thm
             suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
           |> Thm.close_derivation;
 
-        val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
+        val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (As @ Bs @ ss)
+          (fold_rev Logic.all (Bs @ ss)
             (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
           (K (mk_least_min_alg_tac def least_min_algs_thm))
           |> Thm.close_derivation;
 
         val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
 
-        val incl_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
-        val incl_min_algs = map (mk_min_alg passive_UNIVs ss) ks;
+        val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
+        val incl_min_algs = map (mk_min_alg ss) ks;
         val incl = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss)
             (Logic.mk_implies (incl_prem,
@@ -813,7 +804,7 @@
     val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
       (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
         Abs_IIT $ (HOLogic.mk_prod (HOLogic.mk_tuple II_Bs, HOLogic.mk_tuple II_ss))),
-        mk_alg passive_UNIVs II_Bs II_ss)));
+        mk_alg II_Bs II_ss)));
 
     val select_Bs = map (mk_nthN n (HOLogic.mk_fst (Rep_IIT $ iidx))) ks;
     val select_ss = map (mk_nthN n (HOLogic.mk_snd (Rep_IIT $ iidx))) ks;
@@ -850,23 +841,23 @@
     val str_init_defs = map (fn def =>
       mk_unabs_def 2 (Morphism.thm phi def RS meta_eq_to_obj_eq)) str_init_def_frees;
 
-    val car_inits = map (mk_min_alg passive_UNIVs str_inits) ks;
+    val car_inits = map (mk_min_alg str_inits) ks;
 
     (*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
     val alg_init_thm = Goal.prove_sorry lthy [] []
-      (HOLogic.mk_Trueprop (mk_alg passive_UNIVs car_inits str_inits))
+      (HOLogic.mk_Trueprop (mk_alg car_inits str_inits))
       (K (rtac alg_min_alg_thm 1))
       |> Thm.close_derivation;
 
     val alg_select_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_Ball II
-        (Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
+        (Term.absfree iidx' (mk_alg select_Bs select_ss))))
       (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
       |> Thm.close_derivation;
 
     val mor_select_thm =
       let
-        val alg_prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+        val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
         val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss Bs ss Asuc_fs);
         val prems = [alg_prem, i_prem, mor_prem];
@@ -883,7 +874,7 @@
 
     val (init_ex_mor_thm, init_unique_mor_thms) =
       let
-        val prem = HOLogic.mk_Trueprop (mk_alg passive_UNIVs Bs ss);
+        val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val concl = HOLogic.mk_Trueprop
           (list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
         val ex_mor = Goal.prove_sorry lthy [] []
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2013
 
-Compatibility layer with the old datatype package.
+Compatibility layer with the old datatype package ("datatype_compat").
 *)
 
 signature BNF_LFP_COMPAT =
@@ -32,7 +32,7 @@
     fun not_mutually_recursive ss =
       error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
 
-    val (fpT_names as fpT_name1 :: _) =
+    val fpT_names =
       map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
 
     fun lfp_sugar_of s =
@@ -40,7 +40,7 @@
         SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
       | _ => not_datatype s);
 
-    val {ctr_sugars = fp_ctr_sugars, ...} = lfp_sugar_of fpT_name1;
+    val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
     val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars;
     val fpT_names' = map (fst o dest_Type) fpTs0;
 
@@ -52,7 +52,7 @@
 
     fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk =
       (case try lfp_sugar_of s of
-        SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>
+        SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ...}) =>
         let
           val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) [];
           val substT = Term.typ_subst_TVars rho;
@@ -88,7 +88,7 @@
               #>> pair parent_Tkks'
             end;
 
-          val ctrss = map #ctrs ctr_sugars;
+          val ctrss = map (#ctrs o #ctr_sugar o lfp_sugar_of o fst o dest_Type) mutual_Ts;
           val ctr_Tsss = map (map (binder_types o substT o fastype_of)) ctrss;
         in
           ([], kk + mutual_nn)
@@ -107,7 +107,7 @@
     val kkssss = map snd Tparentss_kkssss;
 
     val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts;
-    val ctrss0 = map (#ctrs o of_fp_sugar #ctr_sugars) fp_sugars0;
+    val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0;
     val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0;
 
     fun apply_comps n kk =
@@ -132,9 +132,8 @@
       else
         ((fp_sugars0, (NONE, NONE)), lthy);
 
-    val {ctr_sugars, co_inducts = [induct], co_inductss = inductss, co_iterss,
-      co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars;
-    val inducts = map the_single inductss;
+    val {common_co_inducts = [induct], ...} :: _ = fp_sugars;
+    val inducts = map (the_single o #co_inducts) fp_sugars;
 
     fun mk_dtyp [] (TFree a) = Datatype_Aux.DtTFree a
       | mk_dtyp [] (Type (s, Ts)) = Datatype_Aux.DtType (s, map (mk_dtyp []) Ts)
@@ -148,23 +147,19 @@
       (kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0));
 
     val descr = map3 mk_typ_descr kkssss Tparentss ctrss0;
-    val recs = map (fst o dest_Const o co_rec_of) co_iterss;
-    val rec_thms = flat (map co_rec_of iter_thmsss);
+    val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
+    val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
 
-    fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) =
-      let
-        val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,
-          split, split_asm, ...} = nth ctr_sugars index;
-      in
-        (T_name0,
-         {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct,
-         inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
-         rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
-         case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
-         split_asm = split_asm})
-      end;
+    fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar as {casex, exhaust, nchotomy, injects,
+        distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
+      (T_name0,
+       {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
+       inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
+       rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
+       case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
+       split_asm = split_asm});
 
-    val infos = map mk_info (take nn_fp fp_sugars);
+    val infos = map_index mk_info (take nn_fp fp_sugars);
 
     val all_notes =
       (case lfp_sugar_thms of
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -3,7 +3,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2013
 
-Recursor sugar.
+Recursor sugar ("primrec").
 *)
 
 signature BNF_LFP_REC_SUGAR =
@@ -134,32 +134,59 @@
     massage_call
   end;
 
-fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+type basic_lfp_sugar =
+  {T: typ,
+   fp_res_index: int,
+   ctor_iters: term list,
+   ctr_defs: thm list,
+   ctr_sugar: ctr_sugar,
+   iters: term list,
+   iter_thmss: thm list list};
+
+fun basic_lfp_sugar_of ({T, fp_res = {xtor_co_iterss = ctor_iterss, ...}, fp_res_index, ctr_defs,
+    ctr_sugar, co_iters = iters, co_iter_thmss = iter_thmss, ...} : fp_sugar) =
+  {T = T, fp_res_index = fp_res_index, ctor_iters = nth ctor_iterss fp_res_index,
+   ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, iters = iters, iter_thmss = iter_thmss};
+
+fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
   let
-    val thy = Proof_Context.theory_of lthy0;
-
     val ((missing_arg_Ts, perm0_kks,
           fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...},
             co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy) =
       nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy0;
+    val nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs;
+    val nested_map_comps = map map_comp_of_bnf nested_bnfs;
+  in
+    (missing_arg_Ts, perm0_kks, map basic_lfp_sugar_of fp_sugars, nested_map_idents,
+     nested_map_comps, ctor_iters1, induct_thm, lfp_sugar_thms, lthy)
+  end;
 
-    val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
+fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
+  let
+    val thy = Proof_Context.theory_of lthy0;
 
-    val indices = map #index fp_sugars;
-    val perm_indices = map #index perm_fp_sugars;
+    val (missing_arg_Ts, perm0_kks, basic_lfp_sugars, nested_map_idents, nested_map_comps,
+         ctor_iters1, induct_thm, lfp_sugar_thms, lthy) =
+      get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0;
+
+    val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
 
-    val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
+    val indices = map #fp_res_index basic_lfp_sugars;
+    val perm_indices = map #fp_res_index perm_basic_lfp_sugars;
+
+    val perm_ctrss = map (#ctrs o #ctr_sugar) perm_basic_lfp_sugars;
     val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
-    val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
 
     val nn0 = length arg_Ts;
-    val nn = length perm_lfpTs;
+    val nn = length perm_ctrss;
     val kks = 0 upto nn - 1;
+
     val perm_ns = map length perm_ctr_Tsss;
     val perm_mss = map (map length) perm_ctr_Tsss;
+    val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
 
-    val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res))
-      perm_fp_sugars;
+    val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
+    val perm_Cs = map (body_type o fastype_of o co_rec_of o #ctor_iters) perm_basic_lfp_sugars;
     val perm_fun_arg_Tssss =
       mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
 
@@ -170,6 +197,7 @@
 
     val lfpTs = unpermute perm_lfpTs;
     val Cs = unpermute perm_Cs;
+    val ctr_offsets = unpermute perm_ctr_offsets;
 
     val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
     val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
@@ -181,10 +209,6 @@
 
     val perm_Cs' = map substCT perm_Cs;
 
-    fun offset_of_ctr 0 _ = 0
-      | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
-        length ctrs + offset_of_ctr (n - 1) ctr_sugars;
-
     fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) (i, substACT T)
       | call_of [i, i'] [T, T'] = Mutual_Rec ((i, substACT T), (i', substACT T'));
 
@@ -198,24 +222,18 @@
          rec_thm = rec_thm}
       end;
 
-    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
-      let
-        val ctrs = #ctrs (nth ctr_sugars index);
-        val rec_thms = co_rec_of (nth iter_thmsss index);
-        val k = offset_of_ctr index ctr_sugars;
-        val n = length ctrs;
-      in
-        map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thms
-      end;
+    fun mk_ctr_specs fp_res_index k ctrs rec_thms =
+      map4 mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
+        rec_thms;
 
-    fun mk_spec ({T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...}
-      : fp_sugar) =
-      {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
-       nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
-       nested_map_comps = map map_comp_of_bnf nested_bnfs,
-       ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
+    fun mk_spec ctr_offset
+        ({T, fp_res_index, ctr_sugar = {ctrs, ...}, iters, iter_thmss, ...} : basic_lfp_sugar) =
+      {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of iters),
+       nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
+       ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs (co_rec_of iter_thmss)};
   in
-    ((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms), lthy)
+    ((is_some lfp_sugar_thms, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm,
+      induct_thms), lthy)
   end;
 
 val undef_const = Const (@{const_name undefined}, dummyT);
@@ -501,10 +519,11 @@
 
     val actual_nn = length funs_data;
 
-    val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
+    val ctrs = maps (map #ctr o #ctr_specs) rec_specs;
+    val _ =
       map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
         primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^
-          " is not a constructor in left-hand side") user_eqn) eqns_data end;
+          " is not a constructor in left-hand side") user_eqn) eqns_data;
 
     val defs = build_defs lthy bs mxs funs_data rec_specs has_call;
 
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -89,16 +89,13 @@
 val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
 
 fun mk_alg_set_tac alg_def =
-  dtac (alg_def RS iffD1) 1 THEN
-  REPEAT_DETERM (etac conjE 1) THEN
-  EVERY' [etac bspec, rtac CollectI] 1 THEN
-  REPEAT_DETERM (etac conjI 1) THEN atac 1;
+  EVERY' [dtac (alg_def RS iffD1), REPEAT_DETERM o etac conjE, etac bspec, rtac CollectI,
+   REPEAT_DETERM o (rtac (subset_UNIV RS conjI) ORELSE' etac conjI), atac] 1;
 
 fun mk_alg_not_empty_tac ctxt alg_set alg_sets wits =
   (EVERY' [rtac notI, hyp_subst_tac ctxt, ftac alg_set] THEN'
   REPEAT_DETERM o FIRST'
-    [rtac subset_UNIV,
-    EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
+    [EVERY' [rtac @{thm subset_emptyI}, eresolve_tac wits],
     EVERY' [rtac subsetI, rtac FalseE, eresolve_tac wits],
     EVERY' [rtac subsetI, dresolve_tac wits, hyp_subst_tac ctxt,
       FIRST' (map (fn thm => rtac thm THEN' atac) alg_sets)]] THEN'
@@ -220,7 +217,7 @@
       CONJ_WRAP' (fn (thms, thm) =>
         EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
           rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm,
-          REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
+          REPEAT_DETERM_N n o set_tac thms])
       (set_maps ~~ alg_sets);
   in
     (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
@@ -238,7 +235,7 @@
     val mor_tac =
       CONJ_WRAP' (fn (thms, thm) =>
         EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm,
-          REPEAT_DETERM o rtac subset_UNIV, REPEAT_DETERM_N n o (set_tac thms)])
+          REPEAT_DETERM_N n o set_tac thms])
       (set_maps ~~ alg_sets);
   in
     (rtac (iso_alt RS iffD2) THEN'
@@ -340,7 +337,7 @@
     fun mk_minH_tac (min_alg, alg_set) = EVERY' [rtac ord_eq_le_trans, etac min_alg,
       rtac @{thm Un_least}, minG_tac, rtac @{thm image_subsetI},
       REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac alg_set,
-      REPEAT_DETERM o FIRST' [atac, etac subset_trans THEN' minG_tac]];
+      REPEAT_DETERM o (etac subset_trans THEN' minG_tac)];
   in
     (rtac induct THEN'
     rtac impI THEN'
@@ -397,9 +394,8 @@
     fun alg_epi_tac ((alg_set, str_init_def), set_map) =
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
         rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set,
-        REPEAT_DETERM o FIRST' [rtac subset_UNIV,
-          EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans,
-            etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]]];
+        REPEAT_DETERM o EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans,
+            etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]];
   in
     (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}) THEN'
     rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
@@ -448,7 +444,6 @@
 
     fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
       REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
-      REPEAT_DETERM_N m o rtac subset_UNIV,
       REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
       rtac trans, mor_tac morE in_mono,
       rtac trans, cong_tac map_cong0,
@@ -468,7 +463,6 @@
 
     fun mk_alg_tac alg_set = EVERY' [rtac ballI, rtac CollectI,
       REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
-      REPEAT_DETERM_N m o rtac subset_UNIV,
       REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
       rtac mp, etac bspec, rtac CollectI,
       REPEAT_DETERM_N m o (rtac conjI THEN' atac),
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -1059,8 +1059,8 @@
 (* Give the inner timeout a chance. *)
 val timeout_bonus = seconds 1.0
 
-fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
-                      step subst def_assm_ts nondef_assm_ts orig_t =
+fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
+                      subst def_assm_ts nondef_assm_ts orig_t =
   let
     val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
     val print_t = if mode = TPTP then Output.urgent_message else K ()
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -791,8 +791,7 @@
       val ctrs2 =
         (case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of
            SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
-           map dest_Const
-               (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
+           map dest_Const (#ctrs (#ctr_sugar fp_sugar))
          | _ => [])
     in
       exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T)
@@ -937,7 +936,7 @@
        (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
           SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
           map (apsnd (repair_constr_type T) o dest_Const)
-              (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
+              (#ctrs (#ctr_sugar fp_sugar))
         | _ =>
           if is_frac_type ctxt T then
             case typedef_info ctxt s of
@@ -1465,12 +1464,12 @@
                                        |> the |> #3 |> length))
                 (Datatype.get_all thy) [] @
     map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @
-    maps (fn {fp, ctr_sugars, ...} =>
-             if fp = BNF_FP_Util.Greatest_FP then
-               map (apsnd num_binder_types o dest_Const o #casex) ctr_sugars
-             else
-               [])
-         (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
+    map_filter (fn {fp, ctr_sugar = {casex, ...}, ...} =>
+                   if fp = BNF_FP_Util.Greatest_FP then
+                     SOME (apsnd num_binder_types (dest_Const casex))
+                   else
+                     NONE)
+        (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
   end
 
 fun fixpoint_kind_of_const thy table x =
diff -r 88c40aff747d -r 439d40b226d1 src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Feb 18 20:50:07 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Tue Feb 18 21:00:13 2014 +0100
@@ -31,7 +31,6 @@
 val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0))
 val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0))
 val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0))
-val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
 val struct_atom1_atom1_v1 =
   FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])