# HG changeset patch
# User haftmann
# Date 1747851223 -7200
# Node ID e153ab596247086bbb79739d0669b618a2a213aa
# Parent  f03b71078a47708785e08ec3e5ca4b3c788ef5f4
provide modern interface for loopers

diff -r f03b71078a47 -r e153ab596247 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Wed May 21 20:13:43 2025 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed May 21 20:13:43 2025 +0200
@@ -1038,12 +1038,11 @@
 
 text \<open>
   \begin{mldecls}
-  @{define_ML_infix setloop: "Proof.context *
-  (Proof.context -> int -> tactic) -> Proof.context"} \\
-  @{define_ML_infix addloop: "Proof.context *
-  (string * (Proof.context -> int -> tactic))
-  -> Proof.context"} \\
-  @{define_ML_infix delloop: "Proof.context * string -> Proof.context"} \\
+  @{define_ML Simplifier.set_loop: "(Proof.context -> int -> tactic) ->
+  Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.add_loop: "string * (Proof.context -> int -> tactic) ->
+  Proof.context -> Proof.context"} \\
+  @{define_ML Simplifier.del_loop: "string -> Proof.context -> Proof.context"} \\
   @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
   @{define_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
   @{define_ML Splitter.add_split_bang: "
@@ -1060,14 +1059,14 @@
   Another possibility is to apply an elimination rule on the assumptions. More
   adventurous loopers could start an induction.
 
-    \<^descr> \<open>ctxt setloop tac\<close> installs \<open>tac\<close> as the only looper tactic of \<open>ctxt\<close>.
+    \<^descr> \<^ML>\<open>Simplifier.set_loop\<close>~\<open>tac ctxt\<close> installs \<open>tac\<close> as the only looper tactic of \<open>ctxt\<close>.
 
-    \<^descr> \<open>ctxt addloop (name, tac)\<close> adds \<open>tac\<close> as an additional looper tactic
+    \<^descr> \<^ML>\<open>Simplifier.add_loop\<close>~\<open>(name, tac) ctxt\<close> adds \<open>tac\<close> as an additional looper tactic
     with name \<open>name\<close>, which is significant for managing the collection of
     loopers. The tactic will be tried after the looper tactics that had
     already been present in \<open>ctxt\<close>.
 
-    \<^descr> \<open>ctxt delloop name\<close> deletes the looper tactic that was associated with
+    \<^descr> \<^ML>\<open>Simplifier.del_loop\<close>~\<open>name ctxt\<close> deletes the looper tactic that was associated with
     \<open>name\<close> from \<open>ctxt\<close>.
 
     \<^descr> \<^ML>\<open>Splitter.add_split\<close>~\<open>thm ctxt\<close> adds split tactic
diff -r f03b71078a47 -r e153ab596247 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed May 21 20:13:43 2025 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed May 21 20:13:43 2025 +0200
@@ -102,10 +102,13 @@
   val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
   val prems_of: Proof.context -> thm list
   val add_prems: thm list -> Proof.context -> Proof.context
+  val loop_tac: Proof.context -> int -> tactic
+  val set_loop: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
+  val add_loop: string * (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
+  val del_loop: string -> Proof.context -> Proof.context
   val solvers: Proof.context -> solver list * solver list
   val solver: Proof.context -> solver -> int -> tactic
   val set_solvers: solver list -> Proof.context -> Proof.context
-  val loop_tac: Proof.context -> int -> tactic
   val default_mk_sym: Proof.context -> thm -> thm option
   val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
     Proof.context -> Proof.context
@@ -868,22 +871,28 @@
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, _, loop_tacs, solvers) =>
    (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers));
 
-fun ctxt setloop tac = ctxt |>
+fun set_loop tac =
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) =>
    (congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers));
 
-fun ctxt addloop (name, tac) = ctxt |>
+fun ctxt setloop tac = ctxt |> set_loop tac;
+
+fun add_loop (name, tac) =
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac,
      AList.update (op =) (name, tac) loop_tacs, solvers));
 
-fun ctxt delloop name = ctxt |>
+fun ctxt addloop tac = ctxt |> add_loop tac;
+
+fun del_loop name ctxt = ctxt |>
   map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac,
      (if AList.defined (op =) loop_tacs name then ()
       else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name);
       AList.delete (op =) name loop_tacs), solvers));
 
+fun ctxt delloop name = ctxt |> del_loop name;
+
 fun ctxt setSSolver solver = ctxt |> map_simpset2
   (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
     (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));