diff -r 55c85d25e18c -r 4f5ab843cf5b src/HOL/Auth/All_Symmetric.thy
--- a/src/HOL/Auth/All_Symmetric.thy	Thu Dec 10 21:31:24 2015 +0100
+++ b/src/HOL/Auth/All_Symmetric.thy	Thu Dec 10 21:39:33 2015 +0100
@@ -2,7 +2,7 @@
 imports Message
 begin
 
-text {* All keys are symmetric *}
+text \<open>All keys are symmetric\<close>
 
 defs all_symmetric_def: "all_symmetric \<equiv> True"