--- a/src/HOL/SET_Protocol/Event_SET.thy Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy Mon Nov 10 21:49:48 2014 +0100
@@ -182,14 +182,14 @@
ML
{*
-val analz_mono_contra_tac =
+fun analz_mono_contra_tac ctxt =
rtac @{thm analz_impI} THEN'
REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
- THEN' mp_tac
+ THEN' mp_tac ctxt
*}
method_setup analz_mono_contra = {*
- Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
"for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
end