1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Wed Nov 06 13:00:16 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Wed Nov 06 13:00:45 2013 +0100
     1.3 @@ -69,7 +69,6 @@
     1.4  
     1.5  type corec_spec =
     1.6    {corec: term,
     1.7 -   nested_maps: thm list,
     1.8     nested_map_idents: thm list,
     1.9     nested_map_comps: thm list,
    1.10     ctr_specs: corec_ctr_spec list};
    1.11 @@ -343,18 +342,6 @@
    1.12        end)
    1.13    | _ => not_codatatype ctxt res_T);
    1.14  
    1.15 -(*FIXME: remove special cases for product and sum once they are registered as datatypes*)
    1.16 -fun map_thms_of_typ ctxt (Type (s, _)) =
    1.17 -    if s = @{type_name prod} then
    1.18 -      @{thms map_pair_simp}
    1.19 -    else if s = @{type_name sum} then
    1.20 -      @{thms sum_map.simps}
    1.21 -    else
    1.22 -      (case fp_sugar_of ctxt s of
    1.23 -        SOME {index, mapss, ...} => nth mapss index
    1.24 -      | NONE => [])
    1.25 -  | map_thms_of_typ _ _ = [];
    1.26 -
    1.27  fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
    1.28    let
    1.29      val thy = Proof_Context.theory_of lthy;
    1.30 @@ -449,7 +436,6 @@
    1.31            disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
    1.32          p_is q_isss f_isss f_Tsss =
    1.33        {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
    1.34 -       nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
    1.35         nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
    1.36         nested_map_comps = map map_comp_of_bnf nested_bnfs,
    1.37         ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
    1.38 @@ -947,8 +933,8 @@
    1.39                |> single
    1.40              end;
    1.41  
    1.42 -        fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
    1.43 -            : corec_spec) (disc_eqns : coeqn_data_disc list) exclsss
    1.44 +        fun prove_sel ({nested_map_idents, nested_map_comps, ctr_specs, ...} : corec_spec)
    1.45 +            (disc_eqns : coeqn_data_disc list) exclsss
    1.46              ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, ...} : coeqn_data_sel) =
    1.47            let
    1.48              val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs;
    1.49 @@ -968,8 +954,8 @@
    1.50                |> curry Logic.list_all (map dest_Free fun_args);
    1.51              val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
    1.52            in
    1.53 -            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
    1.54 -              nested_map_idents nested_map_comps sel_corec k m exclsss
    1.55 +            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents
    1.56 +              nested_map_comps sel_corec k m exclsss
    1.57              |> K |> Goal.prove lthy [] [] t
    1.58              |> Thm.close_derivation
    1.59              |> pair sel

     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Wed Nov 06 13:00:16 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Wed Nov 06 13:00:45 2013 +0100
     2.3 @@ -15,7 +15,7 @@
     2.4    val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
     2.5      thm list -> int list -> thm list -> tactic
     2.6    val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
     2.7 -    thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
     2.8 +    thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
     2.9  end;
    2.10  
    2.11  structure BNF_GFP_Rec_Sugar_Tactics : BNF_GFP_REC_SUGAR_TACTICS =
    2.12 @@ -63,7 +63,7 @@
    2.13  fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
    2.14    mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
    2.15  
    2.16 -fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms maps map_idents map_comps f_sel k m
    2.17 +fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps f_sel k m
    2.18      exclsss =
    2.19    mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
    2.20    mk_primcorec_cases_tac ctxt k m exclsss THEN
    2.21 @@ -75,7 +75,7 @@
    2.22      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    2.23      etac notE THEN' atac ORELSE'
    2.24      (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
    2.25 -      (@{thms id_def o_def split_def sum.cases} @ maps @ map_comps @ map_idents)))));
    2.26 +      (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
    2.27  
    2.28  fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
    2.29    HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'