--- 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"})