src/HOL/Real/rat_arith.ML

--- a/src/HOL/Real/rat_arith.ML	Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Real/rat_arith.ML	Mon Oct 17 23:10:13 2005 +0200
@@ -49,6 +49,6 @@
                       addsimprocs simprocs}),
   arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT),
   arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT),
-  Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]];
+  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy)];
 
 end;