src/HOL/SET_Protocol/Purchase.thy

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