--- a/src/HOL/Tools/lin_arith.ML Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Aug 25 18:36:22 2010 +0200
@@ -910,7 +910,7 @@
val setup =
init_arith_data #>
- Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc (@{theory}) "fast_nat_arith"
+ Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc_global (@{theory}) "fast_nat_arith"
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K simproc)]
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
useful to detect inconsistencies among the premises for subgoals which are