src/HOL/Tools/Function/induction_schema.ML

 
             val cqs = map (Thm.cterm_of ctxt o Free) qs
             val ags = map (Thm.assume o Thm.cterm_of ctxt) gs
 
             val replace_x_simpset =
-              put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps)
+              put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps (branch_hyp :: case_hyps)
             val sih = full_simplify replace_x_simpset aihyp
 
             fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
               let
                 val cGas = map (Thm.assume o Thm.cterm_of ctxt) Gas