src/HOL/Hyperreal/hypreal_arith.ML

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