1.1 --- a/src/HOL/Library/Numeral_Type.thy	Fri Oct 30 13:59:52 2009 +0100
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Fri Oct 30 14:00:43 2009 +0100
     1.3 @@ -188,7 +188,7 @@
     1.4  by (rule type_definition.Abs_inverse [OF type])
     1.5  
     1.6  lemma Rep_Abs_mod: "Rep (Abs (m mod n)) = m mod n"
     1.7 -by (simp add: Abs_inverse IntDiv.pos_mod_conj [OF size0])
     1.8 +by (simp add: Abs_inverse pos_mod_conj [OF size0])
     1.9  
    1.10  lemma Rep_Abs_0: "Rep (Abs 0) = 0"
    1.11  by (simp add: Abs_inverse size0)