# HG changeset patch
# User huffman
# Date 1179877575 -7200
# Node ID 044a1bd3bb2abe709898cf45749ee92a98da1f2b
# Parent  e5670ceef56f56f515b7d393d34507468ee46073
remove redundant simproc

diff -r e5670ceef56f -r 044a1bd3bb2a src/HOL/Real/rat_arith.ML
--- a/src/HOL/Real/rat_arith.ML	Tue May 22 21:32:04 2007 +0200
+++ b/src/HOL/Real/rat_arith.ML	Wed May 23 01:46:15 2007 +0200
@@ -48,7 +48,6 @@
     simpset = simpset addsimps simps
                       addsimprocs simprocs}) #>
   arith_inj_const ("Nat.of_nat", HOLogic.natT --> ratT) #>
-  arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT) #>
-  (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy))
+  arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT)
 
 end;