--- a/src/HOL/Nominal/nominal_inductive.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Apr 17 22:22:21 2008 +0200
@@ -311,8 +311,7 @@
in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
fun mk_ind_proof thy thss =
- let val ctxt = ProofContext.init thy
- in Goal.prove_global thy [] prems' concl' (fn ihyps =>
+ Goal.prove_global thy [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
rtac raw_induct 1 THEN
EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
@@ -404,8 +403,7 @@
REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
etac impE 1 THEN atac 1 THEN REPEAT (etac allE_Nil 1) THEN
asm_full_simp_tac (simpset_of thy) 1)
- end)
- end;
+ end);
(** strong case analysis rule **)
@@ -460,8 +458,8 @@
fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)),
prems') =
- let val ctxt1 = ProofContext.init thy
- in (name, Goal.prove_global thy [] (prem :: prems') concl (fn hyp :: hyps =>
+ (name, Goal.prove_global thy [] (prem :: prems') concl
+ (fn {prems = hyp :: hyps, context = ctxt1} =>
EVERY (rtac (hyp RS elim) 1 ::
map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
SUBPROOF (fn {prems = case_hyps, params, context = ctxt2, concl, ...} =>
@@ -534,7 +532,6 @@
val final = ProofContext.export ctxt3 ctxt2 [th]
in resolve_tac final 1 end) ctxt1 1)
(thss ~~ hyps ~~ prems))))
- end
in
thy |>
--- a/src/HOL/Nominal/nominal_package.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Thu Apr 17 22:22:21 2008 +0200
@@ -1049,7 +1049,7 @@
val dt_induct_prop = DatatypeProp.make_ind descr' sorts';
val dt_induct = Goal.prove_global thy8 []
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rtac indrule_lemma' 1,
(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
@@ -1270,7 +1270,7 @@
val _ = warning "proving strong induction theorem ...";
- val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn prems =>
+ val induct_aux = Goal.prove_global thy9 [] ind_prems' ind_concl' (fn {prems, context} =>
let
val (prems1, prems2) = chop (length dt_atomTs) prems;
val ind_ss2 = HOL_ss addsimps
@@ -1283,7 +1283,7 @@
fin_set_fresh @ calc_atm;
val ind_ss5 = HOL_basic_ss addsimps pt1_atoms;
val ind_ss6 = HOL_basic_ss addsimps flat perm_simps';
- val th = Goal.prove (ProofContext.init thy9) [] [] aux_ind_concl
+ val th = Goal.prove context [] [] aux_ind_concl
(fn {context = context1, ...} =>
EVERY (indtac dt_induct tnames 1 ::
maps (fn ((_, (_, _, constrs)), (_, constrs')) =>
@@ -1369,7 +1369,7 @@
end) fresh_fs) induct_aux;
val induct = Goal.prove_global thy9 [] ind_prems ind_concl
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rtac induct_aux' 1,
REPEAT (resolve_tac fs_atoms 1),
REPEAT ((resolve_tac prems THEN_ALL_NEW
@@ -1552,7 +1552,8 @@
HOLogic.mk_imp (R $ x $ y,
finite $ (Const ("Nominal.supp", U --> aset) $ y))
end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs)))))
- (fn fins => (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
+ (fn {prems = fins, ...} =>
+ (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT
(NominalPermeq.finite_guess_tac (HOL_ss addsimps [fs_name]) 1))))
end) dt_atomTs;
@@ -1992,7 +1993,7 @@
(resolve_tac prems THEN_ALL_NEW atac)
in
Goal.prove_global thy12 [] prems' concl'
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rewrite_goals_tac reccomb_defs,
rtac the1_equality 1,
solve rec_unique_thms prems 1,
--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Apr 17 22:22:21 2008 +0200
@@ -71,7 +71,7 @@
in
SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rtac induct' 1,
REPEAT (rtac TrueI 1),
REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
@@ -383,7 +383,7 @@
let
fun prove_weak_case_cong t =
SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
- (fn prems => EVERY [rtac ((hd prems) RS arg_cong) 1])
+ (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
new_type_names descr sorts thy)
@@ -426,7 +426,7 @@
[(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
in
SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
- (fn prems =>
+ (fn {prems, ...} =>
let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
cut_facts_tac [nchotomy''] 1,
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Apr 17 22:22:21 2008 +0200
@@ -607,7 +607,7 @@
val dt_induct_prop = DatatypeProp.make_ind descr sorts;
val dt_induct = SkipProof.prove_global thy6 []
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rtac indrule_lemma' 1,
(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
--- a/src/HOL/Tools/inductive_realizer.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Apr 17 22:22:21 2008 +0200
@@ -391,7 +391,7 @@
(fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs'));
val rews = map mk_meta_eq
(fst_conv :: snd_conv :: get #rec_thms dt_info);
- val thm = Goal.prove_global thy [] prems concl (fn prems => EVERY
+ val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY
[rtac (#raw_induct ind_info) 1,
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
@@ -450,7 +450,7 @@
val rlz' = strip_all (Logic.unvarify rlz);
val rews = map mk_meta_eq case_thms;
val thm = Goal.prove_global thy []
- (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn prems => EVERY
+ (Logic.strip_imp_prems rlz') (Logic.strip_imp_concl rlz') (fn {prems, ...} => EVERY
[cut_facts_tac [hd prems] 1,
etac elimR 1,
ALLGOALS (asm_simp_tac HOL_basic_ss),
--- a/src/HOL/simpdata.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOL/simpdata.ML Thu Apr 17 22:22:21 2008 +0200
@@ -73,7 +73,7 @@
in Goal.prove_global (Thm.theory_of_thm st) []
[mk_simp_implies (Logic.mk_equals (x, y))]
(mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y))))
- (fn prems => EVERY
+ (fn {prems, ...} => EVERY
[rewrite_goals_tac @{thms simp_implies_def},
REPEAT (ares_tac (@{thm meta_eq_to_obj_eq} ::
map (rewrite_rule @{thms simp_implies_def}) prems) 1)])
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu Apr 17 22:22:21 2008 +0200
@@ -84,7 +84,7 @@
val t' = legacy_infer_term thy t;
val asms = Logic.strip_imp_prems t';
val prop = Logic.strip_imp_concl t';
- fun tac prems =
+ fun tac {prems, context} =
rewrite_goals_tac defs THEN
EVERY (tacs (map (rewrite_rule defs) prems));
in Goal.prove_global thy [] asms prop tac end;
--- a/src/Provers/splitter.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/Provers/splitter.ML Thu Apr 17 22:22:21 2008 +0200
@@ -105,7 +105,7 @@
val lift = Goal.prove_global Pure.thy ["P", "Q", "R"]
[Syntax.read_prop_global Pure.thy "!!x :: 'b. Q(x) == R(x) :: 'c"]
(Syntax.read_prop_global Pure.thy "P(%x. Q(x)) == P(%x. R(x))")
- (fn [prem] => rewtac prem THEN rtac reflexive_thm 1)
+ (fn {prems = [prem], ...} => rewtac prem THEN rtac reflexive_thm 1)
val trlift = lift RS transitive_thm;
val _ $ (P $ _) $ _ = concl_of trlift;
--- a/src/Pure/Isar/skip_proof.ML Thu Apr 17 22:22:19 2008 +0200
+++ b/src/Pure/Isar/skip_proof.ML Thu Apr 17 22:22:21 2008 +0200
@@ -12,7 +12,7 @@
val prove: Proof.context -> string list -> term list -> term ->
({prems: thm list, context: Proof.context} -> tactic) -> thm
val prove_global: theory -> string list -> term list -> term ->
- (thm list -> tactic) -> thm
+ ({prems: thm list, context: Proof.context} -> tactic) -> thm
end;
structure SkipProof: SKIP_PROOF =
@@ -45,6 +45,6 @@
else tac args st);
fun prove_global thy xs asms prop tac =
- Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
+ Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
end;