# HG changeset patch
# User blanchet
# Date 1383739245 -3600
# Node ID 3ffb74b52ed6ad03727af4bcc1fe6a4d5e6a5f05
# Parent  c830ead80c91c0268fe5569391613d6ab35a9ac2
removed dead code

diff -r c830ead80c91 -r 3ffb74b52ed6 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Wed Nov 06 13:00:16 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Wed Nov 06 13:00:45 2013 +0100
@@ -69,7 +69,6 @@
 
 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};
@@ -343,18 +342,6 @@
       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;
@@ -449,7 +436,6 @@
           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
@@ -947,8 +933,8 @@
               |> 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;
@@ -968,8 +954,8 @@
               |> 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
diff -r c830ead80c91 -r 3ffb74b52ed6 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Wed Nov 06 13:00:16 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Wed Nov 06 13:00:45 2013 +0100
@@ -15,7 +15,7 @@
   val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
     thm list -> int list -> thm list -> tactic
   val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
-    thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
+    thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
 end;
 
 structure BNF_GFP_Rec_Sugar_Tactics : BNF_GFP_REC_SUGAR_TACTICS =
@@ -63,7 +63,7 @@
 fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
   mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms maps map_idents map_comps f_sel k m
+fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps f_sel k m
     exclsss =
   mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
   mk_primcorec_cases_tac ctxt k m exclsss THEN
@@ -75,7 +75,7 @@
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
-      (@{thms id_def o_def split_def sum.cases} @ maps @ map_comps @ map_idents)))));
+      (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
 
 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
   HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'