--- a/src/ZF/Integ/IntDiv.thy Sun Jan 30 20:48:50 2005 +0100
+++ b/src/ZF/Integ/IntDiv.thy Tue Feb 01 18:01:57 2005 +0100
@@ -1204,7 +1204,7 @@
apply (subgoal_tac "b$*q = r' $- r $+ b'$*q'")
prefer 2 apply (simp add: zcompare_rls)
apply (simp (no_asm_simp) add: zadd_zmult_distrib2)
-apply (subst zadd_commute, rule zadd_zless_mono)
+apply (subst zadd_commute [of "b $\<times> q'"], rule zadd_zless_mono)
prefer 2 apply (blast intro: zmult_zle_mono1)
apply (subgoal_tac "r' $+ #0 $< b $+ r")
apply (simp add: zcompare_rls)