--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 15 12:47:52 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 15 12:48:10 2016 +0100
@@ -2594,8 +2594,7 @@
val (set_induct_thms, set_induct_attrss) =
derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars)
(map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts
- (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss)
- dtor_ctors abs_inverses
+ (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss) dtor_ctors abs_inverses
|> split_list;
val simp_thmss =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Feb 15 12:47:52 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Mon Feb 15 12:48:10 2016 +0100
@@ -104,11 +104,11 @@
(take k (nth excludesss (k - 1))))
end;
-fun prelude_tac ctxt defs thm =
- unfold_thms_tac ctxt defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets;
+fun prelude_tac ctxt fun_defs thm =
+ unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac ctxt thm) THEN unfold_thms_tac ctxt unfold_lets;
-fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss =
- prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss;
+fun mk_primcorec_disc_tac ctxt fun_defs corec_disc k m excludesss =
+ prelude_tac ctxt fun_defs corec_disc THEN cases_tac ctxt k m excludesss;
fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
distinct_discs =
@@ -129,9 +129,9 @@
resolve_tac ctxt
(map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' assume_tac ctxt));
-fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k
- m excludesss =
- prelude_tac ctxt defs (fun_sel RS trans) THEN
+fun mk_primcorec_sel_tac ctxt fun_defs distincts splits split_asms mapsx map_ident0s map_comps
+ fun_sel k m excludesss =
+ prelude_tac ctxt fun_defs (fun_sel RS trans) THEN
cases_tac ctxt k m excludesss THEN
HEADGOAL (REPEAT_DETERM o (rtac ctxt refl ORELSE'
eresolve_tac ctxt falseEs ORELSE'
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Feb 15 12:47:52 2016 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Feb 15 12:48:10 2016 +0100
@@ -469,8 +469,7 @@
val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
- val ((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))) =
- no_defs_lthy
+ val (((((((((u, exh_y), xss), yss), fs), gs), w), (p, p'))), _) = no_defs_lthy
|> add_bindings
|> yield_singleton (mk_Frees fc_b_name) fcT
||>> yield_singleton (mk_Frees "y") fcT (* for compatibility with "datatype_realizer.ML" *)
@@ -479,8 +478,7 @@
||>> mk_Frees "f" case_Ts
||>> mk_Frees "g" case_Ts
||>> yield_singleton (mk_Frees "z") B
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT
- |> fst;
+ ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
val q = Free (fst p', mk_pred1T B);
@@ -679,8 +677,7 @@
fun after_qed ([exhaust_thm] :: thmss) lthy =
let
- val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) =
- lthy
+ val ((((((((u, u'), (xss, xss')), fs), gs), h), v), p), _) = lthy
|> add_bindings
|> yield_singleton (apfst (op ~~) oo mk_Frees' fc_b_name) fcT
||>> mk_Freess' "x" ctr_Tss