# HG changeset patch
# User wenzelm
# Date 1294442911 -3600
# Node ID 0e4f6cf20cdf5c2c884550518817c0d0ecb48fb3
# Parent  8fc17c5e11c096148f8eefae29331c2de72ed05a
tuned;

diff -r 8fc17c5e11c0 -r 0e4f6cf20cdf src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Jan 08 00:02:11 2011 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sat Jan 08 00:28:31 2011 +0100
@@ -891,7 +891,7 @@
 
 val setup =
   init_arith_data #>
-  Simplifier.map_ss (fn ss => ss addsimprocs [Simplifier.simproc_global (@{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