diff -r 4bee6d8c1500 -r 26bf09b95dda src/HOL/SET_Protocol/Event_SET.thy
--- 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