src/HOL/SET_Protocol/Purchase.thy

 method_setup valid_certificate_tac = {*
   Args.goal_spec >> (fn quant =>
     K (SIMPLE_METHOD'' quant (fn i =>
       EVERY [ftac @{thm Gets_certificate_valid} i,
              assume_tac i, REPEAT (hyp_subst_tac i)])))
-*} ""
+*}
 
 
 subsection{*Proofs on Symmetric Keys*}
 
 text{*Nobody can have used non-existent keys!*}