diff -r 0c5cd369a643 -r 50b60f501b05 src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -262,7 +262,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
 *}
 
@@ -333,7 +333,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}])