src/HOL/Bali/Eval.thy

--- a/src/HOL/Bali/Eval.thy	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Bali/Eval.thy	Thu Jun 12 12:44:47 2025 +0200
@@ -774,7 +774,7 @@
 
 declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *)
 declare split_paired_All [simp del] split_paired_Ex [simp del]
-setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
+setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.del_loop "split_all_tac")\<close>
 
 inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v, s')"
 
@@ -812,7 +812,7 @@
         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> (x, s')"
 declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
 declare split_paired_All [simp] split_paired_Ex [simp]
-declaration \<open>K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\<close>
+declaration \<open>K (Simplifier.map_ss (fn ss => ss |> Simplifier.add_loop ("split_all_tac", split_all_tac)))\<close>
 declare if_split     [split] if_split_asm     [split] 
         option.split [split] option.split_asm [split]