src/HOL/Tools/int_arith.ML
changeset 38715 6513ea67d95d
parent 36945 9bec62c10714
child 38763 283f1f9969ba
     1.1 --- a/src/HOL/Tools/int_arith.ML	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -79,7 +79,7 @@
     1.4    proc = sproc, identifier = []}
     1.5  
     1.6  val fast_int_arith_simproc =
     1.7 -  Simplifier.simproc @{theory} "fast_int_arith"
     1.8 +  Simplifier.simproc_global @{theory} "fast_int_arith"
     1.9       ["(m::'a::{linordered_idom,number_ring}) < n",
    1.10        "(m::'a::{linordered_idom,number_ring}) <= n",
    1.11        "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);