diff -r d81094515061 -r b9c92f384109 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Real/real_arith.ML	Mon Oct 17 23:10:13 2005 +0200
@@ -127,7 +127,7 @@
     simpset = simpset addsimps simps}),
   arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
   arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
-  Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
+  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)];
 
 (* some thms for injection nat => real:
 real_of_nat_zero