src/HOL/UNITY/Simple/NSP_Bad.thy

--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -110,7 +110,7 @@
       full_simp_tac ctxt 1,
       REPEAT (FIRSTGOAL (etac disjE)),
       ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])),
-      REPEAT (FIRSTGOAL analz_mono_contra_tac),
+      REPEAT (FIRSTGOAL (analz_mono_contra_tac ctxt)),
       ALLGOALS (asm_simp_tac ctxt)]) i;
 
 (*Tactic for proving secrecy theorems*)