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