diff -r 3d3d24186352 -r 3078fd2eec7b src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Sep 06 10:01:27 2006 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Wed Sep 06 13:48:02 2006 +0200
@@ -9,7 +9,7 @@
 header{*The Division Operators div and mod; the Divides Relation dvd*}
 
 theory IntDiv
-imports SetInterval Recdef
+imports "../SetInterval" "../Recdef"
 uses ("IntDiv_setup.ML")
 begin
 
@@ -959,7 +959,7 @@
           (if b=bit.B0 | (0::int) \<le> number_of w                    
            then number_of v div (number_of w)     
            else (number_of v + (1::int)) div (number_of w))"
-apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
+apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 
 apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 
             split: bit.split)
 done
@@ -1001,7 +1001,7 @@
         | bit.B1 => if (0::int) \<le> number_of w  
                 then 2 * (number_of v mod number_of w) + 1     
                 else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
-apply (simp only: number_of_eq Bin_simps UNIV_I split: bit.split) 
+apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split) 
 apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
                  not_0_le_lemma neg_zmod_mult_2 add_ac)
 done