diff -r f30b73385060 -r 25b068a99d2b src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/IMPP/Hoare.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -381,7 +381,6 @@
 apply (drule finite_subset)
 apply (erule finite_imageI)
 apply (simp (no_asm_simp))
-apply arith
 done
 
 lemma MGT_BodyN: "insert ({=}.BODY pn.{->}) G|-{=}. the (body pn) .{->} ==>