src/HOL/Tools/Function/scnp_reconstruct.ML

   gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
 
 fun decomp_scnp_tac orders ctxt =
   let
     val extra_simps = Named_Theorems.get ctxt \<^named_theorems>\<open>termination_simp\<close>
-    val autom_tac = auto_tac (ctxt addsimps extra_simps)
+    val autom_tac = auto_tac (ctxt |> Simplifier.add_simps extra_simps)
   in
      gen_sizechange_tac orders autom_tac ctxt
   end