src/HOL/Auth/Guard/Guard_Public.thy

--- a/src/HOL/Auth/Guard/Guard_Public.thy	Mon Dec 28 21:47:32 2015 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy	Mon Dec 28 23:13:33 2015 +0100
@@ -14,7 +14,7 @@
 subsubsection\<open>signature\<close>
 
 definition sign :: "agent => msg => msg" where
-"sign A X == {|Agent A, X, Crypt (priK A) (Hash X)|}"
+"sign A X == \<lbrace>Agent A, X, Crypt (priK A) (Hash X)\<rbrace>"
 
 lemma sign_inj [iff]: "(sign A X = sign A' X') = (A=A' & X=X')"
 by (auto simp: sign_def)