theorems need names

--- a/src/HOL/Auth/Shared.thy	Tue Oct 04 09:19:17 2005 +0200
+++ b/src/HOL/Auth/Shared.thy	Tue Oct 04 09:58:17 2005 +0200
@@ -103,7 +103,8 @@
 lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K"
 by blast
 
-declare shrK_neq [THEN not_sym, simp]
+lemmas shrK_sym_neq = shrK_neq [THEN not_sym]
+declare shrK_sym_neq [simp]
 
 
 subsection{*Fresh nonces*}