# HG changeset patch
# User blanchet
# Date 1380150307 -7200
# Node ID 3d93e8b4ae0264d9dd1e4b30ebc1f5cd9b7ce771
# Parent  527ece7edc51b06d45a8a2944d2615a1ef12dea1
tuning

diff -r 527ece7edc51 -r 3d93e8b4ae02 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 26 01:05:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Sep 26 01:05:07 2013 +0200
@@ -273,11 +273,11 @@
 val mk_fp_iter_fun_types = binder_fun_types o fastype_of;
 
 fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
-  | unzip_recT _ (T as Type (@{type_name prod}, Ts)) = Ts
+  | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
   | unzip_recT _ T = [T];
 
 fun unzip_corecT (Type (@{type_name sum}, _)) T = [T]
-  | unzip_corecT _ (T as Type (@{type_name sum}, Ts)) = Ts
+  | unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts
   | unzip_corecT _ T = [T];
 
 fun mk_map live Ts Us t =
@@ -458,7 +458,7 @@
   (mk_coiter_p_pred_types Cs ns,
    mk_fp_iter_fun_types dtor_coiter |> mk_coiter_fun_arg_types0 ctr_Tsss Cs ns);
 
-fun mk_coiters_args_types ctr_Tsss Cs ns mss dtor_coiter_fun_Tss lthy =
+fun mk_coiters_args_types ctr_Tsss Cs ns dtor_coiter_fun_Tss lthy =
   let
     val p_Tss = mk_coiter_p_pred_types Cs ns;
 
@@ -524,7 +524,7 @@
       if fp = Least_FP then
         mk_iters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (rpair NONE o SOME)
       else
-        mk_coiters_args_types ctr_Tsss Cs ns mss xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME)
+        mk_coiters_args_types ctr_Tsss Cs ns xtor_co_iter_fun_Tss lthy |>> (pair NONE o SOME)
   in
     ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
   end;
diff -r 527ece7edc51 -r 3d93e8b4ae02 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 01:05:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 01:05:07 2013 +0200
@@ -206,7 +206,7 @@
       val indirect_calls' = tag_list 0 calls
         |> map_filter (try (apsnd (fn Indirect_Rec n => n)));
 
-      fun make_direct_type T = dummyT; (* FIXME? *)
+      fun make_direct_type _ = dummyT; (* FIXME? *)
 
       val rec_res_type_list = map (fn (x :: _) => (#rec_type x, #res_type x)) funs_data;
 
@@ -801,8 +801,8 @@
               |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
               |> curry Logic.list_all (map dest_Free fun_args);
           in
-            mk_primcorec_ctr_or_sel_tac lthy def_thms sel_corec k m exclsss
-              nested_maps nested_map_idents nested_map_comps [] []
+            mk_primcorec_sel_tac lthy def_thms sel_corec k m exclsss nested_maps nested_map_idents
+              nested_map_comps [] []
             |> K |> Goal.prove lthy [] [] t
             |> pair sel
           end;
diff -r 527ece7edc51 -r 3d93e8b4ae02 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 01:05:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 01:05:07 2013 +0200
@@ -11,12 +11,10 @@
   val mk_primcorec_code_tac: thm list -> thm list -> thm -> thm list -> tactic
   val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> int list -> thm list -> tactic
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
-  val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
-    thm list list list -> thm list -> thm list -> thm list -> thm list -> thm list ->tactic
-  val mk_primcorec_disc_of_ctr_tac: thm -> thm -> tactic;
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
-  val mk_primcorec_sel_of_ctr_tac: thm -> thm -> tactic;
+  val mk_primcorec_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
+    thm list list list -> thm list -> thm list -> thm list -> thm list -> thm list ->tactic
   val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
 end;
 
@@ -56,9 +54,8 @@
 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_ctr_or_sel_tac ctxt defs f_eq k m exclsss maps map_idents map_comps splits
-    split_asms =
-  mk_primcorec_prelude ctxt defs (f_eq RS trans) THEN
+fun mk_primcorec_sel_tac ctxt defs f_sel k m exclsss maps map_idents map_comps splits split_asms =
+  mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
   mk_primcorec_cases_tac ctxt k m exclsss THEN
   unfold_thms_tac ctxt (@{thms o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
@@ -73,12 +70,6 @@
     (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
 
-fun mk_primcorec_disc_of_ctr_tac discI f_ctr =
-  HEADGOAL (rtac discI THEN' rtac f_ctr) THEN ALLGOALS atac;
-
-fun mk_primcorec_sel_of_ctr_tac sel f_ctr =
-  HEADGOAL (etac (f_ctr RS arg_cong RS trans) THEN' rtac sel);
-
 fun mk_primcorec_code_of_ctr_case_tac ctxt eq_caseIs m f_ctr =
   HEADGOAL (REPEAT o resolve_tac (@{thm eq_ifI} :: eq_caseIs)) THEN
   mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
diff -r 527ece7edc51 -r 3d93e8b4ae02 src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Thu Sep 26 01:05:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Thu Sep 26 01:05:07 2013 +0200
@@ -67,7 +67,7 @@
 
             val mutual_Ts = map substT mutual_Ts0;
 
-            fun add_interesting_subtypes (U as Type (s, Us)) =
+            fun add_interesting_subtypes (U as Type (_, Us)) =
                 (case filter (exists_subtype_in mutual_Ts) Us of [] => I
                 | Us' => insert (op =) U #> fold add_interesting_subtypes Us')
               | add_interesting_subtypes _ = I;