1.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Tue Dec 09 16:26:47 2008 -0800
     1.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Tue Dec 09 20:35:31 2008 -0800
     1.3 @@ -19,7 +19,7 @@
     1.4  and d = gcd(m,m') and n=m/d and n'=m'/d.
     1.5  *)
     1.6  
     1.7 -val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of_eq_neg}, @{thm le_number_of_eq}];
     1.8 +val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}];
     1.9  
    1.10  local
    1.11    open Int_Numeral_Simprocs