diff -r ef1ddc59b825 -r 7ae4a23b5be6 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Jun 29 17:35:46 2011 +0200
+++ b/src/HOL/Int.thy	Wed Jun 29 18:12:34 2011 +0200
@@ -1545,9 +1545,13 @@
   of_int_0 of_int_1 of_int_add of_int_mult
 
 use "Tools/int_arith.ML"
-setup {* Int_Arith.global_setup *}
 declaration {* K Int_Arith.setup *}
 
+simproc_setup fast_arith ("(m::'a::{linordered_idom,number_ring}) < n" |
+  "(m::'a::{linordered_idom,number_ring}) <= n" |
+  "(m::'a::{linordered_idom,number_ring}) = n") =
+  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
+
 setup {*
   Reorient_Proc.add
     (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)