diff -r b18f417d0b62 -r 16493f0cee9a src/HOL/Integ/IntDiv.ML
--- a/src/HOL/Integ/IntDiv.ML	Tue Dec 19 15:14:36 2000 +0100
+++ b/src/HOL/Integ/IntDiv.ML	Tue Dec 19 15:15:43 2000 +0100
@@ -203,7 +203,7 @@
 	      simpset() addsimps [quorem_def, linorder_neq_iff]));
 qed "divAlg_correct";
 
-(** Aribtrary definitions for division by zero.  Useful to simplify 
+(** Arbitrary definitions for division by zero.  Useful to simplify 
     certain equations **)
 
 Goal "a div (#0::int) = #0";
@@ -912,11 +912,10 @@
 \          else (number_of v + (#1::int)) div (number_of w))";
 by (simp_tac (simpset_of Int.thy addsimps [zadd_assoc, number_of_BIT]) 1);
 by (asm_simp_tac (simpset()
-                  delsimps bin_arith_extra_simps@bin_rel_simps
-		  addsimps [zdiv_zmult_zmult1,
-			    pos_zdiv_mult_2, lemma, neg_zdiv_mult_2]) 1);
+           delsimps [number_of_reorient]@bin_arith_extra_simps@bin_rel_simps
+ 	   addsimps [zdiv_zmult_zmult1, pos_zdiv_mult_2, lemma, 
+                     neg_zdiv_mult_2]) 1);
 qed "zdiv_number_of_BIT";
-
 Addsimps [zdiv_number_of_BIT];