src/HOL/Integ/IntDef.thy

--- a/src/HOL/Integ/IntDef.thy	Tue Aug 29 21:43:34 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Aug 30 03:19:08 2006 +0200
@@ -387,7 +387,7 @@
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
   have "(\<lambda>(x,y). {x-y}) respects intrel"
-    by (simp add: congruent_def)
+    by (simp add: congruent_def) arith
   thus ?thesis
     by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
 qed