diff -r f30b73385060 -r 25b068a99d2b src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -231,7 +231,7 @@
 "greatest_msg other = 0"
 
 lemma greatest_msg_is_greatest: "Nonce n:parts {X} ==> n <= greatest_msg X"
-by (induct X, auto, arith+)
+by (induct X, auto)
 
 subsubsection{*sets of keys*}