--- a/src/HOL/Set.thy Tue Feb 10 17:37:06 2015 +0000
+++ b/src/HOL/Set.thy Wed Feb 11 12:01:56 2015 +0000
@@ -70,12 +70,12 @@
simproc_setup defined_Collect ("{x. P x & Q x}") = {*
fn _ => Quantifier1.rearrange_Collect
- (fn _ =>
- resolve_tac @{thms Collect_cong} 1 THEN
- resolve_tac @{thms iffI} 1 THEN
+ (fn ctxt =>
+ resolve_tac ctxt @{thms Collect_cong} 1 THEN
+ resolve_tac ctxt @{thms iffI} 1 THEN
ALLGOALS
- (EVERY' [REPEAT_DETERM o eresolve_tac @{thms conjE},
- DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
+ (EVERY' [REPEAT_DETERM o eresolve_tac ctxt @{thms conjE},
+ DEPTH_SOLVE_1 o (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms conjI})]))
*}
lemmas CollectE = CollectD [elim_format]
@@ -359,14 +359,14 @@
fn _ => Quantifier1.rearrange_bex
(fn ctxt =>
unfold_tac ctxt @{thms Bex_def} THEN
- Quantifier1.prove_one_point_ex_tac)
+ Quantifier1.prove_one_point_ex_tac ctxt)
*}
simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
fn _ => Quantifier1.rearrange_ball
(fn ctxt =>
unfold_tac ctxt @{thms Ball_def} THEN
- Quantifier1.prove_one_point_all_tac)
+ Quantifier1.prove_one_point_all_tac ctxt)
*}
lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"
@@ -383,7 +383,7 @@
setup {*
map_theory_claset (fn ctxt =>
- ctxt addbefore ("bspec", fn ctxt' => dresolve_tac @{thms bspec} THEN' assume_tac ctxt'))
+ ctxt addbefore ("bspec", fn ctxt' => dresolve_tac ctxt' @{thms bspec} THEN' assume_tac ctxt'))
*}
ML {*