diff -r 31da698fc4e5 -r 6513ea67d95d src/HOL/Tools/lin_arith.ML
--- 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