src/HOL/BNF/Tools/bnf_fp_def_sugar.ML

 
 fun register_fp_sugar key fp_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
 
-fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss'
-    co_induct strong_co_induct co_iter_thmsss lthy =
+fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss co_induct
+    strong_co_induct co_iter_thmsss 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, fp_res = fp_res,
-        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = transpose co_iterss',
+        ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss,
         co_induct = co_induct, strong_co_induct = strong_co_induct, co_iter_thmsss = co_iter_thmsss}
       lthy)) Ts
   |> snd;
 
 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)

      (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
   end;
 
 fun derive_coinduct_coiters_thms_for_types pre_bnfs (dtor_coiters1 :: _) dtor_coinduct
     dtor_strong_induct dtor_ctors [dtor_unfold_thms, dtor_corec_thms] nesting_bnfs nested_bnfs fpTs
-    Cs As kss mss ns ctr_defss ctr_sugars [unfolds, corecs] [unfold_defs, corec_defs] lthy =
-  let
+    Cs As kss mss ns ctr_defss ctr_sugars iterss iter_defss lthy =
+  let
+    val [unfolds, corecs] = transpose iterss;
+    val [unfold_defs, corec_defs] = transpose iter_defss;
+
     val nn = length pre_bnfs;
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
     val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;

            (simpsN, simp_thmss, K [])]
           |> massage_multi_notes;
       in
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
-        |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars iterss' induct_thm
-          induct_thm (transpose [fold_thmss, rec_thmss])
+        |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars (transpose iterss')
+          induct_thm induct_thm (transpose [fold_thmss, rec_thmss])
       end;
 
     fun derive_and_note_coinduct_coiters_thms_for_types
         ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
           (coiterss', coiter_defss')), lthy) =

              (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
              (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
              (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
           derive_coinduct_coiters_thms_for_types pre_bnfs xtor_co_iterss xtor_co_induct
             xtor_strong_co_induct dtor_ctors (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs
-            fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss' coiter_defss' lthy;
+            fpTs Cs As kss mss ns ctr_defss ctr_sugars (transpose coiterss')
+            (transpose coiter_defss') lthy;
 
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
 
         fun flat_coiter_thms coiters disc_coiters sel_coiters =
           coiters @ disc_coiters @ sel_coiters;

            (unfoldN, unfold_thmss, K coiter_attrs)]
           |> massage_multi_notes;
       in
         lthy
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
-        |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars coiterss'
+        |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars (transpose coiterss')
           coinduct_thm strong_coinduct_thm (transpose [unfold_thmss, corec_thmss])
       end;
 
     val lthy' = lthy
       |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~