diff -r f30b73385060 -r 25b068a99d2b src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -35,7 +35,6 @@
       setsum f (lessThan n) <= setsum g (lessThan n)"
 apply (induct_tac "n")
 apply (auto simp add: lessThan_Suc)
-apply (drule_tac x = n in spec, arith)
 done
 
 lemma tokens_mono_prefix [rule_format]: