src/HOL/Analysis/ex/Approximations.thy

   unfolding MACHIN_TAG_def by (simp add: arctan_double power2_eq_square)
 
 ML \<open>
   fun machin_term_conv ctxt ct =
     let
-      val ctxt' = ctxt addsimps @{thms arctan_double' arctan_add_small}
+      val ctxt' = ctxt |> Simplifier.add_simps @{thms arctan_double' arctan_add_small}
     in
       case Thm.term_of ct of
         Const (\<^const_name>\<open>MACHIN_TAG\<close>, _) $ _ $
           (Const (\<^const_name>\<open>Transcendental.arctan\<close>, _) $ _) =>
           Simplifier.rewrite ctxt' ct

     in
       SELECT_GOAL (
         Local_Defs.unfold_tac ctxt
           @{thms tag_machin[THEN eq_reflection] numeral_horner_MACHIN_TAG[THEN eq_reflection]}
         THEN REPEAT (CHANGED (HEADGOAL (CONVERSION conv))))
-      THEN' Simplifier.simp_tac (ctxt addsimps @{thms arctan_add_small arctan_diff_small})
+      THEN' Simplifier.simp_tac (ctxt |> Simplifier.add_simps @{thms arctan_add_small arctan_diff_small})
     end
 \<close>
 
 method_setup machin = \<open>Scan.succeed (SIMPLE_METHOD' o machin_tac)\<close>