--- 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);
*}