src/HOL/SET_Protocol/Cardholder_Registration.thy

--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -539,7 +539,7 @@
   Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
     (fn i =>
       EVERY [ftac @{thm Gets_certificate_valid} i,
-             assume_tac i,
+             assume_tac ctxt i,
              etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
 *}