rationalized internals
authorblanchet
Mon Mar 03 12:48:20 2014 +0100 (2014-03-03)
changeset 5586837b99986d435
parent 55867 79b915f26533
child 55869 54ddb003e128
rationalized internals
src/HOL/BNF_LFP.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_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
     1.1 --- a/src/HOL/BNF_LFP.thy	Mon Mar 03 12:48:20 2014 +0100
     1.2 +++ b/src/HOL/BNF_LFP.thy	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -266,8 +266,13 @@
     1.4  
     1.5  datatype_new 'a F = F0 | F 'a "'a F"
     1.6  datatype_compat F
     1.7 +datatype_new 'a T = T 'a "'a T F"
     1.8  
     1.9  primrec f where
    1.10    "f (F x y) = F x (f y)"
    1.11  
    1.12 +primrec h and g where
    1.13 +  "h (T x ts) = T x (g ts)" |
    1.14 +  "g F0 = F0"
    1.15 +  
    1.16  end
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
     2.3 @@ -1006,9 +1006,9 @@
     2.4          (unsorted_As ~~ transpose set_boss);
     2.5  
     2.6      val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
     2.7 -             dtors = dtors0, xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors,
     2.8 +             dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
     2.9               ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
    2.10 -             xtor_co_iter_thmss, ...},
    2.11 +             xtor_co_rec_thms, ...},
    2.12             lthy)) =
    2.13        fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
    2.14          (map dest_TFree killed_As) fp_eqs no_defs_lthy0
    2.15 @@ -1094,8 +1094,7 @@
    2.16      val mss = map (map length) ctr_Tsss;
    2.17  
    2.18      val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
    2.19 -      mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss (map co_rec_of xtor_co_iterss0)
    2.20 -        lthy;
    2.21 +      mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
    2.22  
    2.23      fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
    2.24                xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
    2.25 @@ -1314,9 +1313,9 @@
    2.26            (recs, rec_defs)), lthy) =
    2.27        let
    2.28          val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, iter_attrs)) =
    2.29 -          derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
    2.30 -            (map co_rec_of xtor_co_iter_thmss) nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss
    2.31 -            abs_inverses type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
    2.32 +          derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct xtor_co_rec_thms
    2.33 +            nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
    2.34 +            abs_inverses ctrss ctr_defss recs rec_defs lthy;
    2.35  
    2.36          val induct_type_attr = Attrib.internal o K o Induct.induct_type;
    2.37  
    2.38 @@ -1359,8 +1358,8 @@
    2.39               (disc_corec_iff_thmss, disc_corec_iff_attrs),
    2.40               (sel_corec_thmsss, sel_corec_attrs)) =
    2.41            derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
    2.42 -            dtor_injects dtor_ctors (map co_rec_of xtor_co_iter_thmss) nesting_bnfs fpTs Cs Xs
    2.43 -            ctrXs_Tsss kss mss ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
    2.44 +            dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
    2.45 +            abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
    2.46              (Proof_Context.export lthy' no_defs_lthy) lthy;
    2.47  
    2.48          val sel_corec_thmss = map flat sel_corec_thmsss;
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:20 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 03 12:48:20 2014 +0100
     3.3 @@ -236,7 +236,8 @@
     3.4        |> mk_Frees' "s" fold_strTs
     3.5        ||>> mk_Frees' "s" rec_strTs;
     3.6  
     3.7 -    val co_iters = of_fp_res #xtor_co_iterss;
     3.8 +    val co_folds = of_fp_res #xtor_co_folds;
     3.9 +    val co_recs = of_fp_res #xtor_co_recs;
    3.10      val ns = map (length o #Ts o #fp_res) fp_sugars;
    3.11  
    3.12      fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
    3.13 @@ -245,11 +246,11 @@
    3.14  
    3.15      val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
    3.16  
    3.17 -    fun force_iter is_rec i TU TU_rec raw_iters =
    3.18 +    fun force_iter is_rec i TU TU_rec raw_fold raw_rec =
    3.19        let
    3.20          val thy = Proof_Context.theory_of lthy;
    3.21  
    3.22 -        val approx_fold = un_fold_of raw_iters
    3.23 +        val approx_fold = raw_fold
    3.24            |> force_typ names_lthy
    3.25              (replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
    3.26          val subst = Term.typ_subst_atomic fold_thetaAs;
    3.27 @@ -269,9 +270,8 @@
    3.28  
    3.29          val js = find_indices Type.could_unify TUs cands;
    3.30          val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
    3.31 -        val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
    3.32        in
    3.33 -        force_typ names_lthy (Tpats ---> TU) iter
    3.34 +        force_typ names_lthy (Tpats ---> TU) (if is_rec then raw_rec else raw_fold)
    3.35        end;
    3.36  
    3.37      fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
    3.38 @@ -286,10 +286,11 @@
    3.39          val i = find_index (fn T => x = T) Xs;
    3.40          val TUiter =
    3.41            (case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
    3.42 -            NONE => nth co_iters i
    3.43 -              |> force_iter is_rec i
    3.44 +            NONE => 
    3.45 +              force_iter is_rec i
    3.46                  (TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
    3.47 -                (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
    3.48 +                (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
    3.49 +                (nth co_folds i) (nth co_recs i)
    3.50            | SOME f => f);
    3.51  
    3.52          val TUs = binder_fun_types (fastype_of TUiter);
    3.53 @@ -373,6 +374,9 @@
    3.54      val un_folds = map (Morphism.term phi) raw_un_folds;
    3.55      val co_recs = map (Morphism.term phi) raw_co_recs;
    3.56  
    3.57 +    val fp_fold_o_maps = of_fp_res #xtor_co_fold_o_map_thms;
    3.58 +    val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
    3.59 +
    3.60      val (xtor_un_fold_thms, xtor_co_rec_thms) =
    3.61        let
    3.62          val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
    3.63 @@ -419,13 +423,9 @@
    3.64  
    3.65          val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
    3.66  
    3.67 -        val fp_xtor_co_iterss = of_fp_res #xtor_co_iter_thmss;
    3.68 -        val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss;
    3.69 -        val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss;
    3.70 +        val fp_xtor_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_co_fold_thms);
    3.71 +        val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
    3.72  
    3.73 -        val fp_co_iter_o_mapss = of_fp_res #xtor_co_iter_o_map_thmss;
    3.74 -        val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss;
    3.75 -        val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss;
    3.76          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
    3.77            map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @
    3.78            @{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
    3.79 @@ -464,12 +464,8 @@
    3.80      (* These results are half broken. This is deliberate. We care only about those fields that are
    3.81         used by "primrec", "primcorecursive", and "datatype_compat". *)
    3.82      val fp_res =
    3.83 -      ({Ts = fpTs,
    3.84 -        bnfs = of_fp_res #bnfs,
    3.85 -        dtors = dtors,
    3.86 -        ctors = ctors,
    3.87 -        xtor_co_iterss = transpose [un_folds, co_recs],
    3.88 -        xtor_co_induct = xtor_co_induct_thm,
    3.89 +      ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors, xtor_co_folds = un_folds,
    3.90 +        xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
    3.91          dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
    3.92          ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
    3.93          ctor_injects = of_fp_res #ctor_injects (*too general types*),
    3.94 @@ -477,9 +473,10 @@
    3.95          xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
    3.96          xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
    3.97          xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
    3.98 -        xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
    3.99 -        xtor_co_iter_o_map_thmss = of_fp_res #xtor_co_iter_o_map_thmss
   3.100 -          (*theorem about old constant*),
   3.101 +        xtor_co_fold_thms = xtor_un_fold_thms,
   3.102 +        xtor_co_rec_thms = xtor_co_rec_thms,
   3.103 +        xtor_co_fold_o_map_thms = fp_fold_o_maps (*theorems about old constants*),
   3.104 +        xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
   3.105          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
   3.106         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   3.107    in
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
     4.3 @@ -223,8 +223,8 @@
     4.4  
     4.5          val fp_absT_infos = map #absT_info fp_sugars0;
     4.6  
     4.7 -        val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
     4.8 -               dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
     4.9 +        val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
    4.10 +               dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
    4.11            fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
    4.12              no_defs_lthy0;
    4.13  
    4.14 @@ -240,10 +240,8 @@
    4.15          val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
    4.16          val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
    4.17  
    4.18 -        val xtor_co_rec_thms = map co_rec_of xtor_co_iter_thmss;
    4.19          val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
    4.20 -          mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss (map co_rec_of xtor_co_iterss0)
    4.21 -            lthy;
    4.22 +          mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
    4.23  
    4.24          fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
    4.25  
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 03 12:48:20 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 03 12:48:20 2014 +0100
     5.3 @@ -13,7 +13,8 @@
     5.4       bnfs: BNF_Def.bnf list,
     5.5       ctors: term list,
     5.6       dtors: term list,
     5.7 -     xtor_co_iterss: term list list,
     5.8 +     xtor_co_folds: term list,
     5.9 +     xtor_co_recs: term list,
    5.10       xtor_co_induct: thm,
    5.11       dtor_ctors: thm list,
    5.12       ctor_dtors: thm list,
    5.13 @@ -22,8 +23,10 @@
    5.14       xtor_map_thms: thm list,
    5.15       xtor_set_thmss: thm list list,
    5.16       xtor_rel_thms: thm list,
    5.17 -     xtor_co_iter_thmss: thm list list,
    5.18 -     xtor_co_iter_o_map_thmss: thm list list,
    5.19 +     xtor_co_fold_thms: thm list,
    5.20 +     xtor_co_rec_thms: thm list,
    5.21 +     xtor_co_fold_o_map_thms: thm list,
    5.22 +     xtor_co_rec_o_map_thms: thm list,
    5.23       rel_xtor_co_induct_thm: thm}
    5.24  
    5.25    val morph_fp_result: morphism -> fp_result -> fp_result
    5.26 @@ -193,7 +196,8 @@
    5.27     bnfs: BNF_Def.bnf list,
    5.28     ctors: term list,
    5.29     dtors: term list,
    5.30 -   xtor_co_iterss: term list list,
    5.31 +   xtor_co_folds: term list,
    5.32 +   xtor_co_recs: term list,
    5.33     xtor_co_induct: thm,
    5.34     dtor_ctors: thm list,
    5.35     ctor_dtors: thm list,
    5.36 @@ -202,18 +206,22 @@
    5.37     xtor_map_thms: thm list,
    5.38     xtor_set_thmss: thm list list,
    5.39     xtor_rel_thms: thm list,
    5.40 -   xtor_co_iter_thmss: thm list list,
    5.41 -   xtor_co_iter_o_map_thmss: thm list list,
    5.42 +   xtor_co_fold_thms: thm list,
    5.43 +   xtor_co_rec_thms: thm list,
    5.44 +   xtor_co_fold_o_map_thms: thm list,
    5.45 +   xtor_co_rec_o_map_thms: thm list,
    5.46     rel_xtor_co_induct_thm: thm};
    5.47  
    5.48 -fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, dtor_ctors,
    5.49 -    ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
    5.50 -    xtor_co_iter_thmss, xtor_co_iter_o_map_thmss, rel_xtor_co_induct_thm} =
    5.51 +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_folds, xtor_co_recs, xtor_co_induct,
    5.52 +    dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
    5.53 +    xtor_rel_thms, xtor_co_fold_thms, xtor_co_rec_thms, xtor_co_fold_o_map_thms,
    5.54 +    xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
    5.55    {Ts = map (Morphism.typ phi) Ts,
    5.56     bnfs = map (morph_bnf phi) bnfs,
    5.57     ctors = map (Morphism.term phi) ctors,
    5.58     dtors = map (Morphism.term phi) dtors,
    5.59 -   xtor_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss,
    5.60 +   xtor_co_folds = map (Morphism.term phi) xtor_co_folds,
    5.61 +   xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
    5.62     xtor_co_induct = Morphism.thm phi xtor_co_induct,
    5.63     dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    5.64     ctor_dtors = map (Morphism.thm phi) ctor_dtors,
    5.65 @@ -222,8 +230,10 @@
    5.66     xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
    5.67     xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
    5.68     xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    5.69 -   xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss,
    5.70 -   xtor_co_iter_o_map_thmss = map (map (Morphism.thm phi)) xtor_co_iter_o_map_thmss,
    5.71 +   xtor_co_fold_thms = map (Morphism.thm phi) xtor_co_fold_thms,
    5.72 +   xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
    5.73 +   xtor_co_fold_o_map_thms = map (Morphism.thm phi) xtor_co_fold_o_map_thms,
    5.74 +   xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
    5.75     rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
    5.76  
    5.77  fun un_fold_of [f, _] = f;
     6.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 03 12:48:20 2014 +0100
     6.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 03 12:48:20 2014 +0100
     6.3 @@ -2600,16 +2600,13 @@
     6.4      val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
     6.5    in
     6.6      timer;
     6.7 -    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
     6.8 -      xtor_co_iterss = transpose [unfolds, corecs],
     6.9 -      xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
    6.10 -      ctor_dtors = ctor_dtor_thms,
    6.11 -      ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    6.12 +    ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_folds = unfolds,
    6.13 +      xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
    6.14 +      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    6.15        xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
    6.16 -      xtor_rel_thms = dtor_Jrel_thms,
    6.17 -      xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
    6.18 -      xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_Jmap_thms, dtor_corec_o_Jmap_thms],
    6.19 -      rel_xtor_co_induct_thm = Jrel_coinduct_thm},
    6.20 +      xtor_rel_thms = dtor_Jrel_thms, xtor_co_fold_thms = dtor_unfold_thms,
    6.21 +      xtor_co_rec_thms = dtor_corec_thms, xtor_co_fold_o_map_thms = dtor_unfold_o_Jmap_thms,
    6.22 +      xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm},
    6.23       lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd)
    6.24    end;
    6.25  
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 03 12:48:20 2014 +0100
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 03 12:48:20 2014 +0100
     7.3 @@ -1854,14 +1854,13 @@
     7.4      val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
     7.5    in
     7.6      timer;
     7.7 -    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
     7.8 -      xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
     7.9 -      ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    7.10 +    ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_folds = folds,
    7.11 +      xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
    7.12 +      ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
    7.13        xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
    7.14 -      xtor_rel_thms = ctor_Irel_thms,
    7.15 -      xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
    7.16 -      xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_Imap_thms, ctor_rec_o_Imap_thms],
    7.17 -      rel_xtor_co_induct_thm = Irel_induct_thm},
    7.18 +      xtor_rel_thms = ctor_Irel_thms, xtor_co_fold_thms = ctor_fold_thms,
    7.19 +      xtor_co_rec_thms = ctor_rec_thms, xtor_co_fold_o_map_thms = ctor_fold_o_Imap_thms,
    7.20 +      xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm},
    7.21       lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd)
    7.22    end;
    7.23