src/HOL/nat_simprocs.ML
changeset 25481 aa16cd919dcc
parent 24630 351a308ab58d
child 25919 8b1c0d434824
--- a/src/HOL/nat_simprocs.ML	Tue Nov 27 21:06:52 2007 +0100
+++ b/src/HOL/nat_simprocs.ML	Wed Nov 28 09:01:34 2007 +0100
@@ -53,7 +53,7 @@
       @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
       @{thm less_nat_number_of}, 
       @{thm Let_number_of}, @{thm nat_number_of}] @
-     arith_simps @ rel_simps;
+     @{thms arith_simps} @ @{thms rel_simps};
 
 fun prep_simproc (name, pats, proc) =
   Simplifier.simproc (the_context ()) name pats proc;