simplified data structure by reducing the incidence of clumsy indices
authorblanchet
Mon Feb 17 22:54:38 2014 +0100 (2014-02-17)
changeset 555390819931d652d
parent 55538 6a5986170c1d
child 55540 892a425c5eaa
simplified data structure by reducing the incidence of clumsy indices
src/HOL/Nitpick.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
     1.1 --- a/src/HOL/Nitpick.thy	Mon Feb 17 18:18:27 2014 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Feb 17 22:54:38 2014 +0100
     1.3 @@ -9,7 +9,9 @@
     1.4  
     1.5  theory Nitpick
     1.6  imports BNF_FP_Base Map Record Sledgehammer
     1.7 -keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
     1.8 +keywords
     1.9 +  "nitpick" :: diag and
    1.10 +  "nitpick_params" :: thy_decl
    1.11  begin
    1.12  
    1.13  typedecl bisim_iterator
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Feb 17 18:18:27 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Feb 17 22:54:38 2014 +0100
     2.3 @@ -10,22 +10,21 @@
     2.4    type fp_sugar =
     2.5      {T: typ,
     2.6       fp: BNF_FP_Util.fp_kind,
     2.7 -     index: int,
     2.8 -     pre_bnfs: BNF_Def.bnf list,
     2.9 +     fp_res_index: int,
    2.10 +     fp_res: BNF_FP_Util.fp_result,
    2.11 +     pre_bnf: BNF_Def.bnf,
    2.12       nested_bnfs: BNF_Def.bnf list,
    2.13       nesting_bnfs: BNF_Def.bnf list,
    2.14 -     fp_res: BNF_FP_Util.fp_result,
    2.15 -     ctr_defss: thm list list,
    2.16 -     ctr_sugars: Ctr_Sugar.ctr_sugar list,
    2.17 -     co_iterss: term list list,
    2.18 -     mapss: thm list list,
    2.19 +     ctr_defs: thm list,
    2.20 +     ctr_sugar: Ctr_Sugar.ctr_sugar,
    2.21 +     co_iters: term list,
    2.22 +     maps: thm list,
    2.23 +     common_co_inducts: thm list,
    2.24       co_inducts: thm list,
    2.25 -     co_inductss: thm list list,
    2.26 -     co_iter_thmsss: thm list list list,
    2.27 -     disc_co_itersss: thm list list list,
    2.28 -     sel_co_iterssss: thm list list list list};
    2.29 +     co_iter_thmss: thm list list,
    2.30 +     disc_co_iterss: thm list list,
    2.31 +     sel_co_itersss: thm list list list};
    2.32  
    2.33 -  val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
    2.34    val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
    2.35    val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
    2.36    val fp_sugar_of: Proof.context -> string -> fp_sugar option
    2.37 @@ -122,38 +121,40 @@
    2.38  type fp_sugar =
    2.39    {T: typ,
    2.40     fp: fp_kind,
    2.41 -   index: int,
    2.42 -   pre_bnfs: bnf list,
    2.43 +   fp_res_index: int,
    2.44 +   fp_res: fp_result,
    2.45 +   pre_bnf: bnf,
    2.46     nested_bnfs: bnf list,
    2.47     nesting_bnfs: bnf list,
    2.48 -   fp_res: fp_result,
    2.49 -   ctr_defss: thm list list,
    2.50 -   ctr_sugars: ctr_sugar list,
    2.51 -   co_iterss: term list list,
    2.52 -   mapss: thm list list,
    2.53 +   ctr_defs: thm list,
    2.54 +   ctr_sugar: Ctr_Sugar.ctr_sugar,
    2.55 +   co_iters: term list,
    2.56 +   maps: thm list,
    2.57 +   common_co_inducts: thm list,
    2.58     co_inducts: thm list,
    2.59 -   co_inductss: thm list list,
    2.60 -   co_iter_thmsss: thm list list list,
    2.61 -   disc_co_itersss: thm list list list,
    2.62 -   sel_co_iterssss: thm list list list list};
    2.63 -
    2.64 -fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
    2.65 +   co_iter_thmss: thm list list,
    2.66 +   disc_co_iterss: thm list list,
    2.67 +   sel_co_itersss: thm list list list};
    2.68  
    2.69 -fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
    2.70 -    ctr_sugars, co_iterss, mapss, co_inducts, co_inductss, co_iter_thmsss, disc_co_itersss,
    2.71 -    sel_co_iterssss} : fp_sugar) =
    2.72 -  {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    2.73 -    nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    2.74 +fun morph_fp_sugar phi ({T, fp, fp_res, fp_res_index, pre_bnf, nested_bnfs, nesting_bnfs, ctr_defs,
    2.75 +    ctr_sugar, co_iters, maps, common_co_inducts, co_inducts, co_iter_thmss, disc_co_iterss,
    2.76 +    sel_co_itersss} : fp_sugar) =
    2.77 +  {T = Morphism.typ phi T,
    2.78 +   fp = fp,
    2.79     fp_res = morph_fp_result phi fp_res,
    2.80 -   ctr_defss = map (map (Morphism.thm phi)) ctr_defss,
    2.81 -   ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    2.82 -   co_iterss = map (map (Morphism.term phi)) co_iterss,
    2.83 -   mapss = map (map (Morphism.thm phi)) mapss,
    2.84 +   fp_res_index = fp_res_index,
    2.85 +   pre_bnf = morph_bnf phi pre_bnf,
    2.86 +   nested_bnfs = map (morph_bnf phi) nested_bnfs,
    2.87 +   nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    2.88 +   ctr_defs = map (Morphism.thm phi) ctr_defs,
    2.89 +   ctr_sugar = morph_ctr_sugar phi ctr_sugar,
    2.90 +   co_iters = map (Morphism.term phi) co_iters,
    2.91 +   maps = map (Morphism.thm phi) maps,
    2.92 +   common_co_inducts = map (Morphism.thm phi) common_co_inducts,
    2.93     co_inducts = map (Morphism.thm phi) co_inducts,
    2.94 -   co_inductss = map (map (Morphism.thm phi)) co_inductss,
    2.95 -   co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
    2.96 -   disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
    2.97 -   sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
    2.98 +   co_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss,
    2.99 +   disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss,
   2.100 +   sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss};
   2.101  
   2.102  val transfer_fp_sugar =
   2.103    morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
   2.104 @@ -183,15 +184,16 @@
   2.105      (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
   2.106  
   2.107  fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
   2.108 -    ctr_sugars co_iterss mapss co_inducts co_inductss co_iter_thmsss disc_co_itersss
   2.109 +    ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss disc_co_itersss
   2.110      sel_co_iterssss lthy =
   2.111    (0, lthy)
   2.112    |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
   2.113 -    register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
   2.114 -        nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
   2.115 -        ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
   2.116 -        co_inductss = co_inductss, co_iter_thmsss = co_iter_thmsss,
   2.117 -        disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss}
   2.118 +    register_fp_sugar s {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk,
   2.119 +        pre_bnf = nth pre_bnfs kk, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
   2.120 +        ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk,
   2.121 +        maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
   2.122 +        co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
   2.123 +        sel_co_itersss = nth sel_co_iterssss kk}
   2.124        lthy)) Ts
   2.125    |> snd;
   2.126  
   2.127 @@ -1407,8 +1409,8 @@
   2.128          |> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
   2.129          |> Local_Theory.notes (common_notes @ notes) |> snd
   2.130          |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
   2.131 -          iterss mapss [induct_thm] (transpose [induct_thms]) (transpose [fold_thmss, rec_thmss])
   2.132 -          [] []
   2.133 +          iterss mapss [induct_thm] (map single induct_thms) (transpose [fold_thmss, rec_thmss])
   2.134 +          (replicate nn []) (replicate nn [])
   2.135        end;
   2.136  
   2.137      fun derive_note_coinduct_coiters_thms_for_types
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 18:18:27 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Feb 17 22:54:38 2014 +0100
     3.3 @@ -47,7 +47,8 @@
     3.4  
     3.5  fun construct_mutualized_fp fp fpTs fp_sugars bs resBs (resDs, Dss) bnfs lthy =
     3.6    let
     3.7 -    fun steal get = map (of_fp_sugar (get o #fp_res)) fp_sugars;
     3.8 +    fun steal_fp_res get =
     3.9 +      map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
    3.10  
    3.11      val n = length bnfs;
    3.12      val deads = fold (union (op =)) Dss resDs;
    3.13 @@ -77,8 +78,8 @@
    3.14  
    3.15      val ((ctors, dtors), (xtor's, xtors)) =
    3.16        let
    3.17 -        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal #ctors);
    3.18 -        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal #dtors);
    3.19 +        val ctors = map2 (force_typ names_lthy o (fn T => dummyT --> T)) fpTs (steal_fp_res #ctors);
    3.20 +        val dtors = map2 (force_typ names_lthy o (fn T => T --> dummyT)) fpTs (steal_fp_res #dtors);
    3.21        in
    3.22          ((ctors, dtors), `(map (Term.subst_atomic_types theta)) (fp_case fp ctors dtors))
    3.23        end;
    3.24 @@ -92,9 +93,8 @@
    3.25        ||>> mk_Frees "x" xTs
    3.26        ||>> mk_Frees "y" yTs;
    3.27  
    3.28 -    val fp_bnfs = steal #bnfs;
    3.29 -    val pre_bnfs = map (of_fp_sugar #pre_bnfs) fp_sugars;
    3.30 -    val pre_bnfss = map #pre_bnfs fp_sugars;
    3.31 +    val fp_bnfs = steal_fp_res #bnfs;
    3.32 +    val pre_bnfs = map #pre_bnf fp_sugars;
    3.33      val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
    3.34      val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
    3.35      val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
    3.36 @@ -126,9 +126,9 @@
    3.37  
    3.38      val pre_rels = map2 (fn Ds => mk_rel_of_bnf Ds (As @ fpTs) (Bs @ fpTs')) Dss bnfs;
    3.39  
    3.40 -    val rel_unfoldss = map (maps (fn bnf => no_refl [rel_def_of_bnf bnf])) pre_bnfss;
    3.41 -    val rel_xtor_co_inducts = steal (split_conj_thm o #rel_xtor_co_induct_thm)
    3.42 -      |> map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) rel_unfoldss;
    3.43 +    val rel_unfolds = maps (no_refl o single o rel_def_of_bnf) pre_bnfs;
    3.44 +    val rel_xtor_co_inducts = steal_fp_res (split_conj_thm o #rel_xtor_co_induct_thm)
    3.45 +      |> map (unfold_thms lthy (id_apply :: rel_unfolds));
    3.46  
    3.47      val rel_defs = map rel_def_of_bnf bnfs;
    3.48      val rel_monos = map rel_mono_of_bnf bnfs;
    3.49 @@ -185,11 +185,13 @@
    3.50        |> mk_Frees' "s" fold_strTs
    3.51        ||>> mk_Frees' "s" rec_strTs;
    3.52  
    3.53 -    val co_iters = steal #xtor_co_iterss;
    3.54 -    val ns = map (length o #pre_bnfs) fp_sugars;
    3.55 +    val co_iters = steal_fp_res #xtor_co_iterss;
    3.56 +    val ns = map (length o #Ts o #fp_res) fp_sugars;
    3.57 +
    3.58      fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
    3.59        | substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
    3.60        | substT _ T = T;
    3.61 +
    3.62      fun force_iter is_rec i TU TU_rec raw_iters =
    3.63        let
    3.64          val approx_fold = un_fold_of raw_iters
    3.65 @@ -325,14 +327,14 @@
    3.66          val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
    3.67          val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
    3.68  
    3.69 -        val map_unfoldss = map (maps (fn bnf => no_refl [map_def_of_bnf bnf])) pre_bnfss;
    3.70 -        val unfold_map = map2 (fn unfs => unfold_thms lthy (id_apply :: unfs)) map_unfoldss;
    3.71 +        val map_unfolds = maps (fn bnf => no_refl [map_def_of_bnf bnf]) pre_bnfs;
    3.72 +        val unfold_map = map (unfold_thms lthy (id_apply :: map_unfolds));
    3.73  
    3.74 -        val fp_xtor_co_iterss = steal #xtor_co_iter_thmss;
    3.75 +        val fp_xtor_co_iterss = steal_fp_res #xtor_co_iter_thmss;
    3.76          val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss |> unfold_map;
    3.77          val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss |> unfold_map;
    3.78  
    3.79 -        val fp_co_iter_o_mapss = steal #xtor_co_iter_o_map_thmss;
    3.80 +        val fp_co_iter_o_mapss = steal_fp_res #xtor_co_iter_o_map_thmss;
    3.81          val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss |> unfold_map;
    3.82          val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss |> unfold_map;
    3.83          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: @{thms id_apply
    3.84 @@ -358,20 +360,21 @@
    3.85         used by "primrec", "primcorecursive", and "datatype_compat". *)
    3.86      val fp_res =
    3.87        ({Ts = fpTs,
    3.88 -        bnfs = steal #bnfs,
    3.89 +        bnfs = steal_fp_res #bnfs,
    3.90          dtors = dtors,
    3.91          ctors = ctors,
    3.92          xtor_co_iterss = transpose [un_folds, co_recs],
    3.93          xtor_co_induct = xtor_co_induct_thm,
    3.94 -        dtor_ctors = steal #dtor_ctors (*too general types*),
    3.95 -        ctor_dtors = steal #ctor_dtors (*too general types*),
    3.96 -        ctor_injects = steal #ctor_injects (*too general types*),
    3.97 -        dtor_injects = steal #dtor_injects (*too general types*),
    3.98 -        xtor_map_thms = steal #xtor_map_thms (*too general types and terms*),
    3.99 -        xtor_set_thmss = steal #xtor_set_thmss (*too general types and terms*),
   3.100 -        xtor_rel_thms = steal #xtor_rel_thms (*too general types and terms*),
   3.101 +        dtor_ctors = steal_fp_res #dtor_ctors (*too general types*),
   3.102 +        ctor_dtors = steal_fp_res #ctor_dtors (*too general types*),
   3.103 +        ctor_injects = steal_fp_res #ctor_injects (*too general types*),
   3.104 +        dtor_injects = steal_fp_res #dtor_injects (*too general types*),
   3.105 +        xtor_map_thms = steal_fp_res #xtor_map_thms (*too general types and terms*),
   3.106 +        xtor_set_thmss = steal_fp_res #xtor_set_thmss (*too general types and terms*),
   3.107 +        xtor_rel_thms = steal_fp_res #xtor_rel_thms (*too general types and terms*),
   3.108          xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
   3.109 -        xtor_co_iter_o_map_thmss = steal #xtor_co_iter_o_map_thmss (*theorem about old constant*),
   3.110 +        xtor_co_iter_o_map_thmss = steal_fp_res #xtor_co_iter_o_map_thmss
   3.111 +          (*theorem about old constant*),
   3.112          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   3.113         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   3.114    in
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Feb 17 18:18:27 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Feb 17 22:54:38 2014 +0100
     4.3 @@ -119,17 +119,18 @@
     4.4      val fp_b_names = map base_name_of_typ fpTs;
     4.5  
     4.6      val nn = length fpTs;
     4.7 +    val kks = 0 upto nn - 1;
     4.8  
     4.9 -    fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) =
    4.10 +    fun target_ctr_sugar_of_fp_sugar fpT ({T, ctr_sugar, ...} : fp_sugar) =
    4.11        let
    4.12          val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) [];
    4.13          val phi = Morphism.term_morphism "BNF" (Term.subst_TVars rho);
    4.14        in
    4.15 -        morph_ctr_sugar phi (nth ctr_sugars index)
    4.16 +        morph_ctr_sugar phi ctr_sugar
    4.17        end;
    4.18  
    4.19 -    val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0;
    4.20 -    val mapss = map (of_fp_sugar #mapss) fp_sugars0;
    4.21 +    val ctr_defss = map #ctr_defs fp_sugars0;
    4.22 +    val mapss = map #maps fp_sugars0;
    4.23      val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
    4.24  
    4.25      val ctrss = map #ctrs ctr_sugars;
    4.26 @@ -215,14 +216,15 @@
    4.27                (mk_binding b) fpTs Cs) fp_bs xtor_co_iterss lthy
    4.28            |>> split_list;
    4.29  
    4.30 -        val ((co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
    4.31 +        val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
    4.32                disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
    4.33            if fp = Least_FP then
    4.34              derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
    4.35                xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
    4.36                co_iterss co_iter_defss lthy
    4.37              |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
    4.38 -              ([induct], [inducts], fold_thmss, rec_thmss, [], [], [], []))
    4.39 +              ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [],
    4.40 +               replicate nn [], replicate nn [], replicate nn []))
    4.41              ||> (fn info => (SOME info, NONE))
    4.42            else
    4.43              derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
    4.44 @@ -232,32 +234,38 @@
    4.45              |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
    4.46                      (disc_unfold_thmss, disc_corec_thmss, _), _,
    4.47                      (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
    4.48 -              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss, corec_thmss,
    4.49 -               disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss))
    4.50 +              (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss,
    4.51 +               corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss,
    4.52 +               sel_corec_thmsss))
    4.53              ||> (fn info => (NONE, SOME info));
    4.54  
    4.55          val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
    4.56  
    4.57 -        fun mk_target_fp_sugar (kk, T) =
    4.58 -          {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
    4.59 -           nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
    4.60 -           ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts,
    4.61 -           co_inductss = transpose co_inductss,
    4.62 -           co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
    4.63 -           disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
    4.64 -           sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
    4.65 +        fun mk_target_fp_sugar T kk pre_bnf ctr_defs ctr_sugar co_iters maps co_inducts un_fold_thms
    4.66 +            co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss sel_corec_thmss =
    4.67 +          {T = T, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
    4.68 +           nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, ctr_defs = ctr_defs,
    4.69 +           ctr_sugar = ctr_sugar, co_iters = co_iters, maps = maps,
    4.70 +           common_co_inducts = common_co_inducts, co_inducts = co_inducts,
    4.71 +           co_iter_thmss = [un_fold_thms, co_rec_thms],
    4.72 +           disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
    4.73 +           sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]}
    4.74            |> morph_fp_sugar phi;
    4.75  
    4.76 -        val n2m_sugar = (map_index mk_target_fp_sugar fpTs, fp_sugar_thms);
    4.77 +        val target_fp_sugars =
    4.78 +          map14 mk_target_fp_sugar fpTs kks pre_bnfs ctr_defss ctr_sugars co_iterss mapss
    4.79 +            (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss disc_corec_thmss
    4.80 +            sel_unfold_thmsss sel_corec_thmsss;
    4.81 +
    4.82 +        val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
    4.83        in
    4.84          (n2m_sugar, lthy |> register_n2m_sugar key n2m_sugar)
    4.85        end)
    4.86    end;
    4.87  
    4.88  (* TODO: needed? *)
    4.89 -fun indexify_callsss fp_sugar callsss =
    4.90 +fun indexify_callsss (fp_sugar as {ctr_sugar = {ctrs, ...}, ...} : fp_sugar) callsss =
    4.91    let
    4.92 -    val {ctrs, ...} = of_fp_sugar #ctr_sugars fp_sugar;
    4.93      fun indexify_ctr ctr =
    4.94        (case AList.lookup Term.aconv_untyped callsss ctr of
    4.95          NONE => replicate (num_binder_types (fastype_of ctr)) []
     5.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Feb 17 18:18:27 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Feb 17 22:54:38 2014 +0100
     5.3 @@ -367,9 +367,7 @@
     5.4    | _ => not_codatatype ctxt res_T);
     5.5  
     5.6  fun map_thms_of_typ ctxt (Type (s, _)) =
     5.7 -    (case fp_sugar_of ctxt s of
     5.8 -      SOME {index, mapss, ...} => nth mapss index
     5.9 -    | NONE => [])
    5.10 +    (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
    5.11    | map_thms_of_typ _ _ = [];
    5.12  
    5.13  fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 =
    5.14 @@ -378,15 +376,15 @@
    5.15  
    5.16      val ((missing_res_Ts, perm0_kks,
    5.17            fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
    5.18 -            co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
    5.19 +            common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
    5.20        nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy0;
    5.21  
    5.22 -    val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
    5.23 +    val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
    5.24  
    5.25 -    val indices = map #index fp_sugars;
    5.26 -    val perm_indices = map #index perm_fp_sugars;
    5.27 +    val indices = map #fp_res_index fp_sugars;
    5.28 +    val perm_indices = map #fp_res_index perm_fp_sugars;
    5.29  
    5.30 -    val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
    5.31 +    val perm_ctrss = map (#ctrs o #ctr_sugar) perm_fp_sugars;
    5.32      val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
    5.33      val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss;
    5.34  
    5.35 @@ -395,8 +393,8 @@
    5.36      val kks = 0 upto nn - 1;
    5.37      val perm_ns = map length perm_ctr_Tsss;
    5.38  
    5.39 -    val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
    5.40 -      of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
    5.41 +    val perm_Cs = map (fn {fp_res, fp_res_index, ...} => domain_type (body_fun_type (fastype_of
    5.42 +      (co_rec_of (nth (#xtor_co_iterss fp_res) fp_res_index))))) perm_fp_sugars;
    5.43      val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) =
    5.44        mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
    5.45  
    5.46 @@ -410,7 +408,7 @@
    5.47      fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
    5.48      fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
    5.49  
    5.50 -    val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
    5.51 +    val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms;
    5.52  
    5.53      val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
    5.54      val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
    5.55 @@ -444,35 +442,32 @@
    5.56           disc_corec = disc_corec, sel_corecs = sel_corecs}
    5.57        end;
    5.58  
    5.59 -    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
    5.60 -        sel_coiterssss =
    5.61 +    fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
    5.62 +        : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss =
    5.63        let
    5.64 -        val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar =
    5.65 -          nth ctr_sugars index;
    5.66          val p_ios = map SOME p_is @ [NONE];
    5.67 -        val discIs = #discIs (nth ctr_sugars index);
    5.68 -        val corec_thms = co_rec_of (nth coiter_thmsss index);
    5.69 -        val disc_corecs = co_rec_of (nth disc_coitersss index);
    5.70 -        val sel_corecss = co_rec_of (nth sel_coiterssss index);
    5.71 +        val corec_thms = co_rec_of coiter_thmss;
    5.72 +        val disc_corecs = co_rec_of disc_coiterss;
    5.73 +        val sel_corecss = co_rec_of sel_coitersss;
    5.74        in
    5.75          map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
    5.76            disc_excludesss collapses corec_thms disc_corecs sel_corecss
    5.77        end;
    5.78  
    5.79 -    fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
    5.80 -          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
    5.81 -        p_is q_isss f_isss f_Tsss =
    5.82 -      {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
    5.83 -       disc_exhausts = #disc_exhausts (nth ctr_sugars index),
    5.84 +    fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters,
    5.85 +        co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss,
    5.86 +        sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
    5.87 +      {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters),
    5.88 +       disc_exhausts = disc_exhausts,
    5.89         nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
    5.90         nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
    5.91         nested_map_comps = map map_comp_of_bnf nested_bnfs,
    5.92 -       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
    5.93 -         disc_coitersss sel_coiterssss};
    5.94 +       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss
    5.95 +         sel_coitersss};
    5.96    in
    5.97      ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
    5.98 -      co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
    5.99 -      strong_co_induct_of coinduct_thmss), lthy)
   5.100 +      co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
   5.101 +      co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss), lthy)
   5.102    end;
   5.103  
   5.104  val undef_const = Const (@{const_name undefined}, dummyT);
     6.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Feb 17 18:18:27 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Feb 17 22:54:38 2014 +0100
     6.3 @@ -2,7 +2,7 @@
     6.4      Author:     Jasmin Blanchette, TU Muenchen
     6.5      Copyright   2013
     6.6  
     6.7 -Compatibility layer with the old datatype package.
     6.8 +Compatibility layer with the old datatype package ("datatype_compat").
     6.9  *)
    6.10  
    6.11  signature BNF_LFP_COMPAT =
    6.12 @@ -32,7 +32,7 @@
    6.13      fun not_mutually_recursive ss =
    6.14        error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
    6.15  
    6.16 -    val (fpT_names as fpT_name1 :: _) =
    6.17 +    val fpT_names =
    6.18        map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
    6.19  
    6.20      fun lfp_sugar_of s =
    6.21 @@ -40,7 +40,7 @@
    6.22          SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
    6.23        | _ => not_datatype s);
    6.24  
    6.25 -    val {ctr_sugars = fp_ctr_sugars, ...} = lfp_sugar_of fpT_name1;
    6.26 +    val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
    6.27      val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars;
    6.28      val fpT_names' = map (fst o dest_Type) fpTs0;
    6.29  
    6.30 @@ -52,7 +52,7 @@
    6.31  
    6.32      fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk =
    6.33        (case try lfp_sugar_of s of
    6.34 -        SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ctr_sugars, ...}) =>
    6.35 +        SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ...}) =>
    6.36          let
    6.37            val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T0, T) Vartab.empty) [];
    6.38            val substT = Term.typ_subst_TVars rho;
    6.39 @@ -88,7 +88,7 @@
    6.40                #>> pair parent_Tkks'
    6.41              end;
    6.42  
    6.43 -          val ctrss = map #ctrs ctr_sugars;
    6.44 +          val ctrss = map (#ctrs o #ctr_sugar o lfp_sugar_of o fst o dest_Type) mutual_Ts;
    6.45            val ctr_Tsss = map (map (binder_types o substT o fastype_of)) ctrss;
    6.46          in
    6.47            ([], kk + mutual_nn)
    6.48 @@ -107,7 +107,7 @@
    6.49      val kkssss = map snd Tparentss_kkssss;
    6.50  
    6.51      val fp_sugars0 = map (lfp_sugar_of o fst o dest_Type) Ts;
    6.52 -    val ctrss0 = map (#ctrs o of_fp_sugar #ctr_sugars) fp_sugars0;
    6.53 +    val ctrss0 = map (#ctrs o #ctr_sugar) fp_sugars0;
    6.54      val ctr_Tsss0 = map (map (binder_types o fastype_of)) ctrss0;
    6.55  
    6.56      fun apply_comps n kk =
    6.57 @@ -132,9 +132,8 @@
    6.58        else
    6.59          ((fp_sugars0, (NONE, NONE)), lthy);
    6.60  
    6.61 -    val {ctr_sugars, co_inducts = [induct], co_inductss = inductss, co_iterss,
    6.62 -      co_iter_thmsss = iter_thmsss, ...} :: _ = fp_sugars;
    6.63 -    val inducts = map the_single inductss;
    6.64 +    val {co_inducts = [induct], ...} :: _ = fp_sugars;
    6.65 +    val inducts = map (the_single o #co_inducts) fp_sugars;
    6.66  
    6.67      fun mk_dtyp [] (TFree a) = Datatype_Aux.DtTFree a
    6.68        | mk_dtyp [] (Type (s, Ts)) = Datatype_Aux.DtType (s, map (mk_dtyp []) Ts)
    6.69 @@ -148,23 +147,19 @@
    6.70        (kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0));
    6.71  
    6.72      val descr = map3 mk_typ_descr kkssss Tparentss ctrss0;
    6.73 -    val recs = map (fst o dest_Const o co_rec_of) co_iterss;
    6.74 -    val rec_thms = flat (map co_rec_of iter_thmsss);
    6.75 +    val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
    6.76 +    val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
    6.77  
    6.78 -    fun mk_info ({T = Type (T_name0, _), index, ...} : fp_sugar) =
    6.79 -      let
    6.80 -        val {casex, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong,
    6.81 -          split, split_asm, ...} = nth ctr_sugars index;
    6.82 -      in
    6.83 -        (T_name0,
    6.84 -         {index = index, descr = descr, inject = injects, distinct = distincts, induct = induct,
    6.85 -         inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
    6.86 -         rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
    6.87 -         case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
    6.88 -         split_asm = split_asm})
    6.89 -      end;
    6.90 +    fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar as {casex, exhaust, nchotomy, injects,
    6.91 +        distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
    6.92 +      (T_name0,
    6.93 +       {index = kk, descr = descr, inject = injects, distinct = distincts, induct = induct,
    6.94 +       inducts = inducts, exhaust = exhaust, nchotomy = nchotomy, rec_names = recs,
    6.95 +       rec_rewrites = rec_thms, case_name = fst (dest_Const casex), case_rewrites = case_thms,
    6.96 +       case_cong = case_cong, weak_case_cong = weak_case_cong, split = split,
    6.97 +       split_asm = split_asm});
    6.98  
    6.99 -    val infos = map mk_info (take nn_fp fp_sugars);
   6.100 +    val infos = map_index mk_info (take nn_fp fp_sugars);
   6.101  
   6.102      val all_notes =
   6.103        (case lfp_sugar_thms of
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Feb 17 18:18:27 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Feb 17 22:54:38 2014 +0100
     7.3 @@ -136,20 +136,17 @@
     7.4  
     7.5  type basic_lfp_sugar =
     7.6    {T: typ,
     7.7 -   index: int,
     7.8 -   ctor_iterss: term list list,
     7.9 -   ctr_defss: thm list list,
    7.10 -   ctr_sugars: Ctr_Sugar.ctr_sugar list,
    7.11 -   iterss: term list list,
    7.12 -   iter_thmsss: thm list list list};
    7.13 +   fp_res_index: int,
    7.14 +   ctor_iters: term list,
    7.15 +   ctr_defs: thm list,
    7.16 +   ctr_sugar: ctr_sugar,
    7.17 +   iters: term list,
    7.18 +   iter_thmss: thm list list};
    7.19  
    7.20 -fun basic_lfp_sugar_of ({T, index, fp_res = {xtor_co_iterss = ctor_iterss, ...}, ctr_defss,
    7.21 -    ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} : fp_sugar) =
    7.22 -  {T = T, index = index, ctor_iterss = ctor_iterss, ctr_defss = ctr_defss,
    7.23 -   ctr_sugars = ctr_sugars, iterss = iterss, iter_thmsss = iter_thmsss};
    7.24 -
    7.25 -fun of_basic_lfp_sugar f (basic_lfp_sugar as ({index, ...} : basic_lfp_sugar)) =
    7.26 -  nth (f basic_lfp_sugar) index;
    7.27 +fun basic_lfp_sugar_of ({T, fp_res = {xtor_co_iterss = ctor_iterss, ...}, fp_res_index, ctr_defs,
    7.28 +    ctr_sugar, co_iters = iters, co_iter_thmss = iter_thmss, ...} : fp_sugar) =
    7.29 +  {T = T, fp_res_index = fp_res_index, ctor_iters = nth ctor_iterss fp_res_index,
    7.30 +   ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, iters = iters, iter_thmss = iter_thmss};
    7.31  
    7.32  fun get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0 =
    7.33    let
    7.34 @@ -172,23 +169,24 @@
    7.35           ctor_iters1, induct_thm, lfp_sugar_thms, lthy) =
    7.36        get_basic_lfp_sugars bs arg_Ts get_indices callssss0 lthy0;
    7.37  
    7.38 -    val perm_basic_lfp_sugars = sort (int_ord o pairself #index) basic_lfp_sugars;
    7.39 +    val perm_basic_lfp_sugars = sort (int_ord o pairself #fp_res_index) basic_lfp_sugars;
    7.40  
    7.41 -    val indices = map #index basic_lfp_sugars;
    7.42 -    val perm_indices = map #index perm_basic_lfp_sugars;
    7.43 +    val indices = map #fp_res_index basic_lfp_sugars;
    7.44 +    val perm_indices = map #fp_res_index perm_basic_lfp_sugars;
    7.45  
    7.46 -    val perm_ctrss = map (#ctrs o of_basic_lfp_sugar #ctr_sugars) perm_basic_lfp_sugars;
    7.47 +    val perm_ctrss = map (#ctrs o #ctr_sugar) perm_basic_lfp_sugars;
    7.48      val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
    7.49 -    val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
    7.50  
    7.51      val nn0 = length arg_Ts;
    7.52 -    val nn = length perm_lfpTs;
    7.53 +    val nn = length perm_ctrss;
    7.54      val kks = 0 upto nn - 1;
    7.55 +
    7.56      val perm_ns = map length perm_ctr_Tsss;
    7.57      val perm_mss = map (map length) perm_ctr_Tsss;
    7.58 +    val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
    7.59  
    7.60 -    val perm_Cs = map (body_type o fastype_of o co_rec_of o of_basic_lfp_sugar #ctor_iterss)
    7.61 -      perm_basic_lfp_sugars;
    7.62 +    val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
    7.63 +    val perm_Cs = map (body_type o fastype_of o co_rec_of o #ctor_iters) perm_basic_lfp_sugars;
    7.64      val perm_fun_arg_Tssss =
    7.65        mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1);
    7.66  
    7.67 @@ -199,6 +197,7 @@
    7.68  
    7.69      val lfpTs = unpermute perm_lfpTs;
    7.70      val Cs = unpermute perm_Cs;
    7.71 +    val ctr_offsets = unpermute perm_ctr_offsets;
    7.72  
    7.73      val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
    7.74      val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
    7.75 @@ -210,10 +209,6 @@
    7.76  
    7.77      val perm_Cs' = map substCT perm_Cs;
    7.78  
    7.79 -    fun offset_of_ctr 0 _ = 0
    7.80 -      | offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) =
    7.81 -        length ctrs + offset_of_ctr (n - 1) ctr_sugars;
    7.82 -
    7.83      fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) (i, substACT T)
    7.84        | call_of [i, i'] [T, T'] = Mutual_Rec ((i, substACT T), (i', substACT T'));
    7.85  
    7.86 @@ -227,22 +222,17 @@
    7.87           rec_thm = rec_thm}
    7.88        end;
    7.89  
    7.90 -    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss =
    7.91 -      let
    7.92 -        val ctrs = #ctrs (nth ctr_sugars index);
    7.93 -        val rec_thms = co_rec_of (nth iter_thmsss index);
    7.94 -        val k = offset_of_ctr index ctr_sugars;
    7.95 -        val n = length ctrs;
    7.96 -      in
    7.97 -        map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thms
    7.98 -      end;
    7.99 +    fun mk_ctr_specs fp_res_index k ctrs rec_thms =
   7.100 +      map4 mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
   7.101 +        rec_thms;
   7.102  
   7.103 -    fun mk_spec ({T, index, ctr_sugars, iterss, iter_thmsss, ...} : basic_lfp_sugar) =
   7.104 -      {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)),
   7.105 +    fun mk_spec ctr_offset
   7.106 +        ({T, fp_res_index, ctr_sugar = {ctrs, ...}, iters, iter_thmss, ...} : basic_lfp_sugar) =
   7.107 +      {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of iters),
   7.108         nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
   7.109 -       ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss};
   7.110 +       ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs (co_rec_of iter_thmss)};
   7.111    in
   7.112 -    ((is_some lfp_sugar_thms, map mk_spec basic_lfp_sugars, missing_arg_Ts, induct_thm,
   7.113 +    ((is_some lfp_sugar_thms, map2 mk_spec ctr_offsets basic_lfp_sugars, missing_arg_Ts, induct_thm,
   7.114        induct_thms), lthy)
   7.115    end;
   7.116  
   7.117 @@ -529,10 +519,11 @@
   7.118  
   7.119      val actual_nn = length funs_data;
   7.120  
   7.121 -    val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
   7.122 +    val ctrs = maps (map #ctr o #ctr_specs) rec_specs;
   7.123 +    val _ =
   7.124        map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
   7.125          primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^
   7.126 -          " is not a constructor in left-hand side") user_eqn) eqns_data end;
   7.127 +          " is not a constructor in left-hand side") user_eqn) eqns_data;
   7.128  
   7.129      val defs = build_defs lthy bs mxs funs_data rec_specs has_call;
   7.130  
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 17 18:18:27 2014 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 17 22:54:38 2014 +0100
     8.3 @@ -1059,8 +1059,8 @@
     8.4  (* Give the inner timeout a chance. *)
     8.5  val timeout_bonus = seconds 1.0
     8.6  
     8.7 -fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
     8.8 -                      step subst def_assm_ts nondef_assm_ts orig_t =
     8.9 +fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
    8.10 +                      subst def_assm_ts nondef_assm_ts orig_t =
    8.11    let
    8.12      val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
    8.13      val print_t = if mode = TPTP then Output.urgent_message else K ()
     9.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 17 18:18:27 2014 +0100
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 17 22:54:38 2014 +0100
     9.3 @@ -791,8 +791,7 @@
     9.4        val ctrs2 =
     9.5          (case BNF_FP_Def_Sugar.fp_sugar_of ctxt co_s of
     9.6             SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
     9.7 -           map dest_Const
     9.8 -               (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
     9.9 +           map dest_Const (#ctrs (#ctr_sugar fp_sugar))
    9.10           | _ => [])
    9.11      in
    9.12        exists (fn (s', T') => s = s' andalso repair_constr_type coT T' = T)
    9.13 @@ -937,7 +936,7 @@
    9.14         (case BNF_FP_Def_Sugar.fp_sugar_of ctxt s of
    9.15            SOME (fp_sugar as {fp = BNF_FP_Util.Greatest_FP, ...}) =>
    9.16            map (apsnd (repair_constr_type T) o dest_Const)
    9.17 -              (#ctrs (BNF_FP_Def_Sugar.of_fp_sugar #ctr_sugars fp_sugar))
    9.18 +              (#ctrs (#ctr_sugar fp_sugar))
    9.19          | _ =>
    9.20            if is_frac_type ctxt T then
    9.21              case typedef_info ctxt s of
    9.22 @@ -1465,12 +1464,12 @@
    9.23                                         |> the |> #3 |> length))
    9.24                  (Datatype.get_all thy) [] @
    9.25      map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt))) @
    9.26 -    maps (fn {fp, ctr_sugars, ...} =>
    9.27 -             if fp = BNF_FP_Util.Greatest_FP then
    9.28 -               map (apsnd num_binder_types o dest_Const o #casex) ctr_sugars
    9.29 -             else
    9.30 -               [])
    9.31 -         (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
    9.32 +    map_filter (fn {fp, ctr_sugar = {casex, ...}, ...} =>
    9.33 +                   if fp = BNF_FP_Util.Greatest_FP then
    9.34 +                     SOME (apsnd num_binder_types (dest_Const casex))
    9.35 +                   else
    9.36 +                     NONE)
    9.37 +        (BNF_FP_Def_Sugar.fp_sugars_of ctxt)
    9.38    end
    9.39  
    9.40  fun fixpoint_kind_of_const thy table x =
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 17 18:18:27 2014 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 17 22:54:38 2014 +0100
    10.3 @@ -31,7 +31,6 @@
    10.4  val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0))
    10.5  val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0))
    10.6  val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0))
    10.7 -val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
    10.8  val struct_atom1_atom1_v1 =
    10.9    FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])
   10.10