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 =