src/HOL/Hyperreal/hypreal_arith.ML

--- a/src/HOL/Hyperreal/hypreal_arith.ML	Mon Oct 17 23:10:10 2005 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML	Mon Oct 17 23:10:13 2005 +0200
@@ -36,7 +36,7 @@
     neqE = neqE,
     simpset = simpset}),
   arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT),
-  Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]];
+  fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy)];
 
 end;