diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/SET_Protocol/Event_SET.thy
--- a/src/HOL/SET_Protocol/Event_SET.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -184,7 +184,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
 *}