src/HOL/Tools/int_arith.ML
changeset 42795 66fcc9882784
parent 38864 4abe644fcea5
child 43595 7ae4a23b5be6
     1.1 --- a/src/HOL/Tools/int_arith.ML	Fri May 13 23:24:06 2011 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Fri May 13 23:58:40 2011 +0200
     1.3 @@ -84,8 +84,8 @@
     1.4        "(m::'a::{linordered_idom,number_ring}) <= n",
     1.5        "(m::'a::{linordered_idom,number_ring}) = n"] (K Lin_Arith.simproc);
     1.6  
     1.7 -val global_setup = Simplifier.map_simpset
     1.8 -  (fn simpset => simpset addsimprocs [fast_int_arith_simproc]);
     1.9 +val global_setup =
    1.10 +  Simplifier.map_simpset_global (fn ss => ss addsimprocs [fast_int_arith_simproc]);
    1.11  
    1.12  
    1.13  fun number_of thy T n =