src/HOL/Real/rat_arith.ML

     lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
     neqE =  neqE,
     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;