src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML

    disc_corec: thm,
    sel_corecs: thm list};
 
 type corec_spec =
   {corec: term,
-   nested_maps: thm list,
    nested_map_idents: thm list,
    nested_map_comps: thm list,
    ctr_specs: corec_ctr_spec list};
 
 exception AINT_NO_MAP of term;

       in
         map3 mk_spec ctrs discs selss
       end)
   | _ => not_codatatype ctxt res_T);
 
-(*FIXME: remove special cases for product and sum once they are registered as datatypes*)
-fun map_thms_of_typ ctxt (Type (s, _)) =
-    if s = @{type_name prod} then
-      @{thms map_pair_simp}
-    else if s = @{type_name sum} then
-      @{thms sum_map.simps}
-    else
-      (case fp_sugar_of ctxt s of
-        SOME {index, mapss, ...} => nth mapss index
-      | NONE => [])
-  | map_thms_of_typ _ _ = [];
-
 fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
     val ((missing_res_Ts, perm0_kks,

 
     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)),
-       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};
   in

               |> Thm.close_derivation
               |> pair (#disc (nth ctr_specs ctr_no))
               |> single
             end;
 
-        fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
-            : corec_spec) (disc_eqns : coeqn_data_disc list) exclsss
+        fun prove_sel ({nested_map_idents, nested_map_comps, ctr_specs, ...} : corec_spec)
+            (disc_eqns : coeqn_data_disc list) exclsss
             ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, ...} : coeqn_data_sel) =
           let
             val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs;
             val ctr_no = find_index (equal ctr o #ctr) ctr_specs;
             val prems = the_default (maps (s_not_conj o #prems) disc_eqns)

               |> HOLogic.mk_Trueprop o HOLogic.mk_eq
               |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
               |> curry Logic.list_all (map dest_Free fun_args);
             val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
           in
-            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
-              nested_map_idents nested_map_comps sel_corec k m exclsss
+            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents
+              nested_map_comps sel_corec k m exclsss
             |> K |> Goal.prove lthy [] [] t
             |> Thm.close_derivation
             |> pair sel
           end;