--- a/src/HOL/Auth/All_Symmetric.thy	Mon Jan 11 21:20:44 2016 +0100
+++ b/src/HOL/Auth/All_Symmetric.thy	Mon Jan 11 21:21:02 2016 +0100
@@ -4,7 +4,10 @@
 
 text \<open>All keys are symmetric\<close>
 
-defs all_symmetric_def: "all_symmetric \<equiv> True"
+overloading all_symmetric \<equiv> all_symmetric
+begin
+  definition "all_symmetric \<equiv> True"
+end
 
 lemma isSym_keys: "K \<in> symKeys"
   by (simp add: symKeys_def all_symmetric_def invKey_symmetric)