diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Auth/Message.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -845,13 +845,13 @@
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)
-val Fake_insert_tac = 
-    dresolve_tac [impOfSubs @{thm Fake_analz_insert},
+fun Fake_insert_tac ctxt = 
+    dresolve_tac ctxt [impOfSubs @{thm Fake_analz_insert},
                   impOfSubs @{thm 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
@@ -869,7 +869,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);
 *}