src/HOL/Tools/Function/mutual.ML

     val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
 
     val induct_inst =
       Thm.forall_elim (Thm.cterm_of ctxt case_exp) induct
       |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
-      |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
+      |> full_simplify (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps all_f_defs)
 
     fun project rule (MutualPart {cargTs, i, ...}) k =
       let
         val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
         val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)

       map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
 
     fun mk_mpsimp fqgar sum_psimp =
       in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
 
-    val rew_simpset = put_simpset HOL_basic_ss lthy addsimps all_f_defs
+    val rew_simpset = put_simpset HOL_basic_ss lthy |> Simplifier.add_simps all_f_defs
     val mpsimps = map2 mk_mpsimp fqgars psimps
     val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
     val mcases = map (mutual_cases_rule lthy cases_rule n ST) parts
     val mtermination = full_simplify rew_simpset termination
     val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros