diff -r ef8ed6adcb38 -r e5434b822a96 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/List.thy	Thu May 30 10:12:52 2002 +0200
@@ -531,7 +531,6 @@
  apply simp_all
 apply(erule ssubst)
 apply auto
-apply arith
 done
 
 lemma in_set_conv_decomp: "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs)"