src/Pure/raw_simplifier.ML

 Higher-order Simplification.
 *)
 
 infix 4
   addsimps delsimps addsimprocs delsimprocs
-  setloop' setloop addloop addloop' delloop
+  setloop addloop delloop
   setSSolver addSSolver setSolver addSolver;
 
 signature BASIC_RAW_SIMPLIFIER =
 sig
   val simp_depth_limit: int Config.T

   val clear_simpset: Proof.context -> Proof.context
   val addsimps: Proof.context * thm list -> Proof.context
   val delsimps: Proof.context * thm list -> Proof.context
   val addsimprocs: Proof.context * simproc list -> Proof.context
   val delsimprocs: Proof.context * simproc list -> Proof.context
-  val setloop': Proof.context * (Proof.context -> int -> tactic) -> Proof.context
-  val setloop: Proof.context * (int -> tactic) -> Proof.context
-  val addloop': Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
-  val addloop: Proof.context * (string * (int -> tactic)) -> Proof.context
+  val setloop: Proof.context * (Proof.context -> int -> tactic) -> Proof.context
+  val addloop: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
   val delloop: Proof.context * string -> Proof.context
   val setSSolver: Proof.context * solver -> Proof.context
   val addSSolver: Proof.context * solver -> Proof.context
   val setSolver: Proof.context * solver -> Proof.context
   val addSolver: Proof.context * solver -> Proof.context

 
 fun set_subgoaler subgoal_tac =
   map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
    (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
 
-fun ctxt setloop' tac = ctxt |>
+fun ctxt setloop tac = ctxt |>
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
    (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
 
-fun ctxt setloop tac = ctxt setloop' (K tac);
-
-fun ctxt addloop' (name, tac) = ctxt |>
+fun ctxt addloop (name, tac) = ctxt |>
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, termless, subgoal_tac,
      AList.update (op =) (name, tac) loop_tacs, solvers));
-
-fun ctxt addloop (name, tac) = ctxt addloop' (name, K tac);
 
 fun ctxt delloop name = ctxt |>
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, termless, subgoal_tac,
      (if AList.defined (op =) loop_tacs name then ()