--- a/src/FOLP/simp.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/FOLP/simp.ML Fri Jul 24 22:16:39 2015 +0200
@@ -36,7 +36,7 @@
val delrews : simpset * thm list -> simpset
val dest_ss : simpset -> thm list * thm list
val print_ss : Proof.context -> simpset -> unit
- val setauto : simpset * (int -> tactic) -> simpset
+ val setauto : simpset * (Proof.context -> int -> tactic) -> simpset
val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic
val ASM_SIMP_TAC : Proof.context -> simpset -> int -> tactic
val CASE_TAC : Proof.context -> simpset -> int -> tactic
@@ -235,14 +235,14 @@
(* SIMPSET *)
datatype simpset =
- SS of {auto_tac: int -> tactic,
+ SS of {auto_tac: Proof.context -> int -> tactic,
congs: thm list,
cong_net: thm Net.net,
mk_simps: Proof.context -> thm -> thm list,
simps: (thm * thm list) list,
simp_net: thm Net.net}
-val empty_ss = SS{auto_tac= K no_tac, congs=[], cong_net=Net.empty,
+val empty_ss = SS{auto_tac= K (K no_tac), congs=[], cong_net=Net.empty,
mk_simps = fn ctxt => normed_rews ctxt [], simps=[], simp_net=Net.empty};
(** Insertion of congruences and rewrites **)
@@ -446,7 +446,7 @@
else (ss,thm,anet,ats,cs);
fun try_true(thm,ss,anet,ats,cs) =
- case Seq.pull(auto_tac i thm) of
+ case Seq.pull(auto_tac ctxt i thm) of
SOME(thm',_) => (ss,thm',anet,ats,cs)
| NONE => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
in if !tracing
@@ -486,7 +486,7 @@
(fn thm =>
if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty
else Seq.single(execute ctxt (ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
- THEN TRY(auto_tac i)
+ THEN TRY(auto_tac ctxt i)
end;
fun SIMP_TAC ctxt = EXEC_TAC ctxt ([MK_EQ,SIMP_LHS,REFL,STOP],false);
--- a/src/FOLP/simpdata.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/FOLP/simpdata.ML Fri Jul 24 22:16:39 2015 +0200
@@ -76,7 +76,7 @@
open FOLP_Simp;
-val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}];
+val auto_ss = empty_ss setauto (fn ctxt => ares_tac ctxt @{thms TrueI});
val IFOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) IFOLP_rews;
--- a/src/HOL/Library/old_recdef.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Fri Jul 24 22:16:39 2015 +0200
@@ -2550,7 +2550,7 @@
*--------------------------------------------------------------------------*)
fun std_postprocessor ctxt strict wfs =
Prim.postprocess ctxt strict
- {wf_tac = REPEAT (ares_tac wfs 1),
+ {wf_tac = REPEAT (ares_tac ctxt wfs 1),
terminator =
asm_simp_tac ctxt 1
THEN TRY (Arith_Data.arith_tac ctxt 1 ORELSE
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Fri Jul 24 22:16:39 2015 +0200
@@ -456,7 +456,7 @@
Object_Logic.atomize_prems_tac ctxt) 1,
rewrite_goals_tac ctxt rewrites,
REPEAT ((resolve_tac ctxt rep_intrs THEN_ALL_NEW
- ((REPEAT o eresolve_tac ctxt [allE]) THEN' ares_tac elem_thms)) 1)]);
+ ((REPEAT o eresolve_tac ctxt [allE]) THEN' ares_tac ctxt elem_thms)) 1)]);
in (inj_thms'' @ inj_thms, elem_thms @ Old_Datatype_Aux.split_conj_thm elem_thm) end;
@@ -573,7 +573,7 @@
dresolve_tac ctxt @{thms box_equals} 1,
REPEAT (resolve_tac ctxt rep_thms 1),
REPEAT (eresolve_tac ctxt inj_thms 1),
- REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (resolve_tac ctxt @{thms ext} 1),
+ REPEAT (ares_tac ctxt [conjI] 1 ORELSE (EVERY [REPEAT (resolve_tac ctxt @{thms ext} 1),
REPEAT (eresolve_tac ctxt (make_elim fun_cong :: inj_thms) 1),
assume_tac ctxt 1]))])
end;
@@ -652,7 +652,7 @@
[REPEAT (eresolve_tac ctxt Abs_inverse_thms 1),
simp_tac (put_simpset HOL_basic_ss ctxt
addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
- DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
+ DEPTH_SOLVE_1 (ares_tac ctxt [prem] 1 ORELSE eresolve_tac ctxt [allE] 1)]))
(prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
val ([(_, [dt_induct'])], thy7) =
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Fri Jul 24 22:16:39 2015 +0200
@@ -178,7 +178,7 @@
(EVERY
[DETERM tac,
REPEAT (eresolve_tac ctxt @{thms ex1E} 1), resolve_tac ctxt @{thms ex1I} 1,
- DEPTH_SOLVE_1 (ares_tac [intr] 1),
+ DEPTH_SOLVE_1 (ares_tac ctxt [intr] 1),
REPEAT_DETERM_N k (eresolve_tac ctxt [thin_rl] 1 THEN rotate_tac 1 1),
eresolve_tac ctxt [elim] 1,
REPEAT_DETERM_N j distinct_tac,
--- a/src/HOL/UNITY/UNITY_tactics.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Jul 24 22:16:39 2015 +0200
@@ -41,7 +41,7 @@
[REPEAT (Always_Int_tac ctxt 1),
eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
+ REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
--- a/src/HOL/ex/MT.thy Thu Jul 23 22:13:42 2015 +0200
+++ b/src/HOL/ex/MT.thy Fri Jul 24 22:16:39 2015 +0200
@@ -276,7 +276,7 @@
(* ############################################################ *)
ML {*
-val infsys_mono_tac = REPEAT (ares_tac (@{thms basic_monos} @ [allI, impI]) 1)
+fun infsys_mono_tac ctxt = REPEAT (ares_tac ctxt (@{thms basic_monos} @ [allI, impI]) 1)
*}
lemma infsys_p1: "P a b ==> P (fst (a,b)) (snd (a,b))"
@@ -395,7 +395,7 @@
lemma eval_fun_mono: "mono(eval_fun)"
unfolding mono_def eval_fun_def
-apply (tactic infsys_mono_tac)
+apply (tactic "infsys_mono_tac @{context}")
done
(* Introduction rules *)
@@ -519,7 +519,7 @@
lemma elab_fun_mono: "mono(elab_fun)"
unfolding mono_def elab_fun_def
-apply (tactic infsys_mono_tac)
+apply (tactic "infsys_mono_tac @{context}")
done
(* Introduction rules *)
@@ -747,7 +747,7 @@
lemma mono_hasty_fun: "mono(hasty_fun)"
unfolding mono_def hasty_fun_def
-apply (tactic infsys_mono_tac)
+apply (tactic "infsys_mono_tac @{context}")
apply blast
done
--- a/src/Provers/quantifier1.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/Provers/quantifier1.ML Fri Jul 24 22:16:39 2015 +0200
@@ -144,7 +144,7 @@
ALLGOALS
(EVERY' [eresolve_tac ctxt [Data.exE], REPEAT_DETERM o eresolve_tac ctxt [Data.conjE],
resolve_tac ctxt [Data.exI],
- DEPTH_SOLVE_1 o ares_tac [Data.conjI]])
+ DEPTH_SOLVE_1 o ares_tac ctxt [Data.conjI]])
end;
(* Proves (! x0..xn. (... & x0 = t & ...) --> P x0) =
@@ -157,7 +157,7 @@
REPEAT o resolve_tac ctxt [Data.impI],
eresolve_tac ctxt [Data.mp],
REPEAT o eresolve_tac ctxt [Data.conjE],
- REPEAT o ares_tac [Data.conjI]]);
+ REPEAT o ares_tac ctxt [Data.conjI]]);
val allcomm = Data.all_comm RS Data.iff_trans;
in
fun prove_one_point_all_tac ctxt =
--- a/src/Pure/tactic.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/Pure/tactic.ML Fri Jul 24 22:16:39 2015 +0200
@@ -27,7 +27,7 @@
val dtac: thm -> int -> tactic
val etac: thm -> int -> tactic
val ftac: thm -> int -> tactic
- val ares_tac: thm list -> int -> tactic
+ val ares_tac: Proof.context -> thm list -> int -> tactic
val solve_tac: Proof.context -> thm list -> int -> tactic
val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
val match_tac: Proof.context -> thm list -> int -> tactic
@@ -144,8 +144,8 @@
fun etac rl = eresolve0_tac [rl];
fun ftac rl = forward0_tac [rl];
-(*Use an assumption or some rules ... A popular combination!*)
-fun ares_tac rules = atac ORELSE' resolve0_tac rules;
+(*Use an assumption or some rules*)
+fun ares_tac ctxt rules = assume_tac ctxt ORELSE' resolve_tac ctxt rules;
fun solve_tac ctxt rules = resolve_tac ctxt rules THEN_ALL_NEW assume_tac ctxt;
--- a/src/ZF/Tools/inductive_package.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Jul 24 22:16:39 2015 +0200
@@ -189,7 +189,7 @@
Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
(fn {context = ctxt, ...} => EVERY
[resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
- REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
+ REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]);
val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
@@ -306,9 +306,9 @@
(*Minimizes backtracking by delivering the correct premise to each goal.
Intro rules with extra Vars in premises still cause some backtracking *)
- fun ind_tac [] 0 = all_tac
- | ind_tac(prem::prems) i =
- DEPTH_SOLVE_1 (ares_tac [prem, @{thm refl}] i) THEN ind_tac prems (i-1);
+ fun ind_tac _ [] 0 = all_tac
+ | ind_tac ctxt (prem::prems) i =
+ DEPTH_SOLVE_1 (ares_tac ctxt [prem, @{thm refl}] i) THEN ind_tac ctxt prems (i-1);
val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
@@ -349,7 +349,7 @@
some premise involves disjunction.*)
REPEAT (FIRSTGOAL (eresolve_tac ctxt [@{thm CollectE}, @{thm exE}, @{thm conjE}]
ORELSE' (bound_hyp_subst_tac ctxt))),
- ind_tac (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
+ ind_tac ctxt (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
val dummy =
if ! Ind_Syntax.trace then
@@ -474,7 +474,7 @@
REPEAT (resolve_tac ctxt @{thms impI} 1) THEN
resolve_tac ctxt [rewrite_rule ctxt all_defs prem] 1 THEN
(*prem must not be REPEATed below: could loop!*)
- DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
+ DEPTH_SOLVE (FIRSTGOAL (ares_tac ctxt [@{thm impI}] ORELSE'
eresolve_tac ctxt (@{thm conjE} :: @{thm mp} :: cmonos))))
) i)
THEN mutual_ind_tac ctxt prems (i-1);
--- a/src/ZF/Tools/typechk.ML Thu Jul 23 22:13:42 2015 +0200
+++ b/src/ZF/Tools/typechk.ML Fri Jul 24 22:16:39 2015 +0200
@@ -102,7 +102,7 @@
fun type_solver_tac ctxt hyps = SELECT_GOAL
(DEPTH_SOLVE (eresolve_tac ctxt @{thms FalseE} 1
ORELSE resolve_from_net_tac ctxt basic_net 1
- ORELSE (ares_tac hyps 1
+ ORELSE (ares_tac ctxt hyps 1
APPEND typecheck_step_tac ctxt)));
val type_solver =
--- a/src/ZF/UNITY/SubstAx.thy Thu Jul 23 22:13:42 2015 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Fri Jul 24 22:16:39 2015 +0200
@@ -355,7 +355,7 @@
(EVERY [REPEAT (Always_Int_tac ctxt 1),
eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
+ REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,