metis proof

--- a/src/HOL/Auth/Message.thy	Mon Oct 27 16:23:54 2008 +0100
+++ b/src/HOL/Auth/Message.thy	Mon Oct 27 18:14:34 2008 +0100
@@ -106,9 +106,7 @@
 subsubsection{*Inverse of keys *}
 
 lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
-apply safe
-apply (drule_tac f = invKey in arg_cong, simp)
-done
+by (metis invKey)
 
 
 subsection{*keysFor operator*}