diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/SET_Protocol/Purchase.thy
--- a/src/HOL/SET_Protocol/Purchase.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/SET_Protocol/Purchase.thy	Sun May 15 17:45:53 2011 +0200
@@ -484,7 +484,7 @@
     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*}