--- 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;
--- 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;
--- 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
--- 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;