src/HOL/Tools/inductive_set.ML

--- a/src/HOL/Tools/inductive_set.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -62,7 +62,8 @@
           | decomp _ = NONE;
         val simp =
           full_simp_tac
-            (put_simpset HOL_basic_ss ctxt addsimps @{thms mem_Collect_eq case_prod_conv}) 1;
+            (put_simpset HOL_basic_ss ctxt
+              |> Simplifier.add_simps @{thms mem_Collect_eq case_prod_conv}) 1;
         fun mk_rew t = (case strip_abs_vars t of
             [] => NONE
           | xs => (case decomp (strip_abs_body t) of
@@ -235,7 +236,7 @@
           end)
   in
     Simplifier.simplify
-      (put_simpset HOL_basic_ss ctxt addsimps @{thms mem_Collect_eq case_prod_conv}
+      (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps @{thms mem_Collect_eq case_prod_conv}
         |> Simplifier.add_proc \<^simproc>\<open>Collect_mem\<close>) thm''
       |> zero_var_indexes |> eta_contract_thm ctxt (equal p)
   end;
@@ -384,7 +385,7 @@
     thm |>
     Thm.instantiate (TVars.empty, Vars.make insts) |>
     Simplifier.full_simplify
-      (put_simpset HOL_basic_ss ctxt addsimps to_set_simps
+      (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps to_set_simps
         |> Simplifier.add_proc (strong_ind_simproc pred_arities)
         |> Simplifier.add_proc \<^simproc>\<open>Collect_mem\<close>) |>
     Rule_Cases.save thm
@@ -489,8 +490,8 @@
                 (HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
                   list_comb (c, params))))))
             (K (REPEAT (resolve_tac lthy @{thms ext} 1) THEN
-              simp_tac (put_simpset HOL_basic_ss lthy addsimps
-                [def, @{thm mem_Collect_eq}, @{thm case_prod_conv}]) 1))
+              simp_tac (put_simpset HOL_basic_ss lthy
+                |> Simplifier.add_simps [def, @{thm mem_Collect_eq}, @{thm case_prod_conv}]) 1))
         in
           lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
             [Attrib.internal \<^here> (K pred_set_conv_att)]),