src/HOL/SET_Protocol/Purchase.thy

--- a/src/HOL/SET_Protocol/Purchase.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -482,7 +482,7 @@
 method_setup valid_certificate_tac = {*
   Args.goal_spec >> (fn quant =>
     fn ctxt => SIMPLE_METHOD'' quant (fn i =>
-      EVERY [ftac @{thm Gets_certificate_valid} i,
+      EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
              assume_tac ctxt i, REPEAT (hyp_subst_tac ctxt i)]))
 *}