diff -r 0c5cd369a643 -r 50b60f501b05 src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -837,13 +837,13 @@
 *)
 fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
 
-val Fake_insert_tac = 
-    dresolve_tac [impOfSubs Fake_analz_insert,
+fun Fake_insert_tac ctxt =
+    dresolve_tac ctxt [impOfSubs Fake_analz_insert,
                   impOfSubs Fake_parts_insert] THEN'
-    eresolve_tac [asm_rl, @{thm synth.Inj}];
+    eresolve_tac ctxt [asm_rl, @{thm synth.Inj}];
 
 fun Fake_insert_simp_tac ctxt i = 
-  REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ctxt i;
+  REPEAT (Fake_insert_tac ctxt i) THEN asm_full_simp_tac ctxt i;
 
 fun atomic_spy_analz_tac ctxt =
   SELECT_GOAL
@@ -859,7 +859,7 @@
            (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
        simp_tac ctxt 1,
-       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
+       REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
 *}