--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 25 23:41:24 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 25 23:01:31 2015 +0200
@@ -1258,8 +1258,9 @@
val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
(Logic.list_implies (prem0 :: prems, eq));
in
- Goal.prove_sorry lthy [] [] goal (K (unfold_thms_tac lthy @{thms simp_implies_def} THEN
- mk_map_cong_tac lthy (#map_cong0 axioms)))
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt @{thms simp_implies_def} THEN
+ mk_map_cong_tac ctxt (#map_cong0 axioms))
|> Thm.close_derivation
end;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 25 23:41:24 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Sep 25 23:01:31 2015 +0200
@@ -445,7 +445,8 @@
HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
in
Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
- (K (mk_mor_comp_tac lthy mor_def mor_image'_thms morE_thms map_comp_id_thms))
+ (fn {context = ctxt, prems = _} =>
+ mk_mor_comp_tac ctxt mor_def mor_image'_thms morE_thms map_comp_id_thms)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy)
end;
@@ -457,7 +458,7 @@
val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
in
Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
- (K ((hyp_subst_tac lthy THEN' assume_tac lthy) 1))
+ (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy)
end;
@@ -597,7 +598,7 @@
HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
in
Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
- (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs le_rel_OOs))
+ (fn {context = ctxt, prems = _} => mk_bis_O_tac ctxt m bis_rel_thm rel_congs le_rel_OOs)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy)
end;
@@ -680,7 +681,8 @@
val sbis_lsbis_thm =
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks)))
- (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
+ (fn {context = ctxt, prems = _} =>
+ mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union_thm bis_cong_thm)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy);
@@ -1102,7 +1104,7 @@
val length_Lev =
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_length_Lev_tac lthy cts Lev_0s Lev_Sucs))
+ (fn {context = ctxt, prems = _} => mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy);
@@ -1176,7 +1178,8 @@
val set_Lev =
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss))
+ (fn {context = ctxt, prems = _} =>
+ mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy);
@@ -1215,8 +1218,9 @@
val set_image_Lev =
Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_set_image_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss
- from_to_sbd_thmss to_sbd_inj_thmss))
+ (fn {context = ctxt, prems = _} =>
+ mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss
+ from_to_sbd_thmss to_sbd_inj_thmss)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy);
@@ -2161,8 +2165,9 @@
fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
- dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
+ (fn {context = ctxt, prems = _} =>
+ mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
+ dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy))
ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss'
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 25 23:41:24 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 25 23:01:31 2015 +0200
@@ -1148,7 +1148,7 @@
fun exclude_tac tac_opt sequential (c, c', a) =
if a orelse c = c' orelse sequential then
- SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
+ SOME (fn {context = ctxt, prems = _} => HEADGOAL (mk_primcorec_assumption_tac ctxt []))
else
tac_opt;
@@ -1233,9 +1233,11 @@
|> list_all_fun_args ps
|> @{map 3} (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
| [nchotomy_thm] => fn [goal] =>
- [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
- (length disc_eqns) nchotomy_thm
- |> K |> Goal.prove_sorry lthy [] [] goal
+ [Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_primcorec_exhaust_tac ctxt
+ ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
+ (length disc_eqns) nchotomy_thm)
|> Thm.close_derivation])
disc_eqnss nchotomy_thmss;
val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
@@ -1267,8 +1269,9 @@
if prems = [@{term False}] then
[]
else
- mk_primcorec_disc_tac lthy def_thms corec_disc k m excludesss
- |> K |> Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_primcorec_disc_tac ctxt def_thms corec_disc k m excludesss)
|> Thm.close_derivation
|> pair (#disc (nth ctr_specs ctr_no))
|> pair eqn_pos
@@ -1297,9 +1300,10 @@
|> curry Logic.list_all (map dest_Free fun_args);
val (distincts, _, _, split_sels, split_sel_asms) = case_thms_of_term lthy rhs_term;
in
- mk_primcorec_sel_tac lthy def_thms distincts split_sels split_sel_asms fp_nesting_maps
- fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss
- |> K |> Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_primcorec_sel_tac ctxt def_thms distincts split_sels split_sel_asms
+ fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss)
|> Thm.close_derivation
|> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
|> pair sel
@@ -1346,8 +1350,9 @@
if prems = [@{term False}] then
[]
else
- mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms
- |> K |> Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_primcorec_ctr_tac ctxt m collapse disc_thm_opt sel_thms)
|> is_some code_rhs_opt ? fold_thms lthy sel_defs (*mildly too aggressive*)
|> Thm.close_derivation
|> pair ctr
@@ -1431,14 +1436,16 @@
val (distincts, discIs, _, split_sels, split_sel_asms) =
case_thms_of_term lthy raw_rhs;
- val raw_code_thm = mk_primcorec_raw_code_tac lthy distincts discIs split_sels
- split_sel_asms ms ctr_thms
- (if exhaustive_code then try the_single nchotomys else NONE)
- |> K |> Goal.prove_sorry lthy [] [] raw_goal
+ val raw_code_thm =
+ Goal.prove_sorry lthy [] [] raw_goal
+ (fn {context = ctxt, prems = _} =>
+ mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms
+ ms ctr_thms (if exhaustive_code then try the_single nchotomys else NONE))
|> Thm.close_derivation;
in
- mk_primcorec_code_tac lthy distincts split_sels raw_code_thm
- |> K |> Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_primcorec_code_tac ctxt distincts split_sels raw_code_thm)
|> Thm.close_derivation
|> single
end)
@@ -1465,9 +1472,10 @@
mk_conjs prems)
|> curry Logic.list_all (map dest_Free fun_args);
in
- mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
- (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss)
- |> K |> Goal.prove_sorry lthy [] [] goal
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} =>
+ mk_primcorec_disc_iff_tac ctxt (map (fst o dest_Free) exhaust_fun_args)
+ (the_single exhaust_thms) disc_thms disc_thmss' (flat distinct_discss))
|> Thm.close_derivation
|> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve lthy thm rule)))
@{thms eqTrueE eq_False[THEN iffD1] notnotD}
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 25 23:41:24 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 25 23:01:31 2015 +0200
@@ -298,7 +298,8 @@
in
map2 (fn goal => fn alg_set =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
+ (fn {context = ctxt, prems = _} =>
+ mk_alg_not_empty_tac ctxt alg_set alg_set_thms wit_thms)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy))
goals alg_set_thms
@@ -606,7 +607,8 @@
val monos =
map2 (fn goal => fn min_algs =>
- Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac lthy min_algs))
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => mk_min_algs_mono_tac ctxt min_algs)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy))
(map mk_mono_goal min_algss) min_algs_thms;
@@ -1255,8 +1257,9 @@
val goal = Logic.list_implies (prems, concl);
in
(Goal.prove_sorry lthy [] [] goal
- (K (mk_ctor_induct_tac lthy m set_mapss init_induct_thm morE_thms mor_Abs_thm
- Rep_inverses Abs_inverses Reps))
+ (fn {context = ctxt, prems = _} =>
+ mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm
+ Rep_inverses Abs_inverses Reps)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy),
rev (Term.add_tfrees goal []))
@@ -1696,8 +1699,9 @@
fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss =>
Goal.prove_sorry lthy [] [] goal
- (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
- ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
+ (fn {context = ctxt, prems = _} =>
+ mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
+ ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss)
|> Thm.close_derivation
|> singleton (Proof_Context.export names_lthy lthy))
ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss'
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Sep 25 23:41:24 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Sep 25 23:01:31 2015 +0200
@@ -552,9 +552,10 @@
|> map_filter (try (fn (x, [y]) =>
(#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
|> map (fn (user_eqn, num_extra_args, rec_thm) =>
- mk_primrec_tac lthy' num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
- def_thms rec_thm
- |> K |> Goal.prove_sorry lthy' [] [] user_eqn
+ Goal.prove_sorry lthy' [] [] user_eqn
+ (fn {context = ctxt, prems = _} =>
+ mk_primrec_tac ctxt num_extra_args fp_nesting_map_ident0s fp_nesting_map_comps
+ def_thms rec_thm)
|> Thm.close_derivation);
in
((js, simps), lthy')
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 25 23:41:24 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 25 23:01:31 2015 +0200
@@ -739,7 +739,8 @@
mk_Trueprop_eq (eta_ufcase, eta_vgcase));
val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
in
- (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
+ (Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ mk_case_cong_tac ctxt uexhaust_thm case_thms),
Goal.prove_sorry lthy [] [] weak_goal (fn {context = ctxt, prems = _} =>
etac ctxt arg_cong 1))
|> apply2 (singleton (Proof_Context.export names_lthy lthy) #>
@@ -762,8 +763,8 @@
(@{map 3} mk_split_disjunct xctrs xss xfs)));
fun prove_split selss goal =
- Goal.prove_sorry lthy [] [] goal (fn _ =>
- mk_split_tac lthy ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ mk_split_tac ctxt ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;
@@ -976,8 +977,8 @@
val uncollapse_thms =
map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
in
- Goal.prove_sorry lthy [] [] goal (fn _ =>
- mk_expand_tac lthy n ms (inst_thm u exhaust_disc_thm)
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ mk_expand_tac ctxt n ms (inst_thm u exhaust_disc_thm)
(inst_thm v exhaust_disc_thm) uncollapse_thms distinct_disc_thmsss
distinct_disc_thmsss')
|> singleton (Proof_Context.export names_lthy lthy)