src/Pure/raw_simplifier.ML
changeset 52037 837211662fb8
parent 51717 9e7d1c139569
child 52082 559e1398b70e
     1.1 --- a/src/Pure/raw_simplifier.ML	Thu May 16 15:21:12 2013 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu May 16 17:39:38 2013 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  infix 4
     1.6    addsimps delsimps addsimprocs delsimprocs
     1.7 -  setloop' setloop addloop addloop' delloop
     1.8 +  setloop addloop delloop
     1.9    setSSolver addSSolver setSolver addSolver;
    1.10  
    1.11  signature BASIC_RAW_SIMPLIFIER =
    1.12 @@ -49,10 +49,8 @@
    1.13    val delsimps: Proof.context * thm list -> Proof.context
    1.14    val addsimprocs: Proof.context * simproc list -> Proof.context
    1.15    val delsimprocs: Proof.context * simproc list -> Proof.context
    1.16 -  val setloop': Proof.context * (Proof.context -> int -> tactic) -> Proof.context
    1.17 -  val setloop: Proof.context * (int -> tactic) -> Proof.context
    1.18 -  val addloop': Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
    1.19 -  val addloop: Proof.context * (string * (int -> tactic)) -> Proof.context
    1.20 +  val setloop: Proof.context * (Proof.context -> int -> tactic) -> Proof.context
    1.21 +  val addloop: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
    1.22    val delloop: Proof.context * string -> Proof.context
    1.23    val setSSolver: Proof.context * solver -> Proof.context
    1.24    val addSSolver: Proof.context * solver -> Proof.context
    1.25 @@ -821,19 +819,15 @@
    1.26    map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
    1.27     (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
    1.28  
    1.29 -fun ctxt setloop' tac = ctxt |>
    1.30 +fun ctxt setloop tac = ctxt |>
    1.31    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
    1.32     (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
    1.33  
    1.34 -fun ctxt setloop tac = ctxt setloop' (K tac);
    1.35 -
    1.36 -fun ctxt addloop' (name, tac) = ctxt |>
    1.37 +fun ctxt addloop (name, tac) = ctxt |>
    1.38    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.39      (congs, procs, mk_rews, termless, subgoal_tac,
    1.40       AList.update (op =) (name, tac) loop_tacs, solvers));
    1.41  
    1.42 -fun ctxt addloop (name, tac) = ctxt addloop' (name, K tac);
    1.43 -
    1.44  fun ctxt delloop name = ctxt |>
    1.45    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.46      (congs, procs, mk_rews, termless, subgoal_tac,