--- a/src/HOL/Auth/Event.thy Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Auth/Event.thy Tue Feb 10 14:48:26 2015 +0100
@@ -272,7 +272,7 @@
{*
fun analz_mono_contra_tac ctxt =
rtac @{thm analz_impI} THEN'
- REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
+ REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra})
THEN' (mp_tac ctxt)
*}
@@ -289,7 +289,7 @@
fun synth_analz_mono_contra_tac ctxt =
rtac @{thm syan_impI} THEN'
REPEAT1 o
- (dresolve_tac
+ (dresolve_tac ctxt
[@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
@{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
@{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])