diff -r fd7ec31f850c -r f591144b0f17 src/HOL/Tools/rat_arith.ML
--- a/src/HOL/Tools/rat_arith.ML	Fri May 08 08:01:09 2009 +0200
+++ b/src/HOL/Tools/rat_arith.ML	Fri May 08 09:48:07 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Real/rat_arith.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   2004 University of Cambridge
 
@@ -10,8 +9,6 @@
 
 local
 
-val simprocs = field_cancel_numeral_factors
-
 val simps =
  [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
   read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
@@ -42,7 +39,7 @@
     lessD = lessD,  (*Can't change lessD: the rats are dense!*)
     neqE =  neqE,
     simpset = simpset addsimps simps
-                      addsimprocs simprocs}) #>
+                      addsimprocs Numeral_Simprocs.field_cancel_numeral_factors}) #>
   arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #>
   arith_inj_const (@{const_name of_int}, @{typ "int => rat"})