--- a/src/CCL/Term.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/CCL/Term.thy Thu May 16 17:39:38 2013 +0200
@@ -204,7 +204,7 @@
method_setup beta_rl = {*
Scan.succeed (fn ctxt =>
SIMPLE_METHOD' (CHANGED o
- simp_tac (ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
+ simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac @{thm letrecB}))))
*}
lemma ifBtrue: "if true then t else u = t"
--- a/src/Doc/IsarRef/Generic.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/Doc/IsarRef/Generic.thy Thu May 16 17:39:38 2013 +0200
@@ -1143,12 +1143,8 @@
text {*
\begin{mldecls}
@{index_ML_op setloop: "Proof.context *
- (int -> tactic) -> Proof.context"} \\
- @{index_ML_op setloop': "Proof.context *
(Proof.context -> int -> tactic) -> Proof.context"} \\
@{index_ML_op addloop: "Proof.context *
- (string * (int -> tactic)) -> Proof.context"} \\
- @{index_ML_op addloop': "Proof.context *
(string * (Proof.context -> int -> tactic))
-> Proof.context"} \\
@{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\
@@ -1169,15 +1165,13 @@
\begin{description}
\item @{text "ctxt setloop tac"} installs @{text "tac"} as the only
- looper tactic of @{text "ctxt"}. The variant @{text "setloop'"}
- allows the tactic to depend on the running Simplifier context.
+ looper tactic of @{text "ctxt"}.
\item @{text "ctxt addloop (name, tac)"} adds @{text "tac"} as an
additional looper tactic with name @{text "name"}, which is
significant for managing the collection of loopers. The tactic will
be tried after the looper tactics that had already been present in
- @{text "ctxt"}. The variant @{text "addloop'"} allows the tactic to
- depend on the running Simplifier context.
+ @{text "ctxt"}.
\item @{text "ctxt delloop name"} deletes the looper tactic that was
associated with @{text "name"} from @{text "ctxt"}.
--- a/src/HOL/Bali/Basis.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/Basis.thy Thu May 16 17:39:38 2013 +0200
@@ -12,7 +12,7 @@
ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
declare split_if_asm [split] option.split [split] option.split_asm [split]
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
declare if_weak_cong [cong del] option.weak_case_cong [cong del]
declare length_Suc_conv [iff]
--- a/src/HOL/Bali/DefiniteAssignment.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Thu May 16 17:39:38 2013 +0200
@@ -884,7 +884,7 @@
declare inj_term_sym_simps [simp del]
declare assigns_if.simps [simp]
declare split_paired_All [simp] split_paired_Ex [simp]
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
(* To be able to eliminate both the versions with the overloaded brackets:
(B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A),
--- a/src/HOL/Bali/Eval.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/Eval.thy Thu May 16 17:39:38 2013 +0200
@@ -818,7 +818,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 {* K (Simplifier.map_ss (fn ss => ss addloop' ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
--- a/src/HOL/Bali/Evaln.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/Evaln.thy Thu May 16 17:39:38 2013 +0200
@@ -238,7 +238,7 @@
option.split [split] option.split_asm [split]
not_None_eq [simp]
split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Simplifier.map_ss (fn ss => ss addloop' ("split_all_tac", split_all_tac))) *}
+declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>
(case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)
--- a/src/HOL/Bali/TypeSafe.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Thu May 16 17:39:38 2013 +0200
@@ -756,7 +756,7 @@
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i;
@@ -925,7 +925,7 @@
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
subsection "accessibility"
--- a/src/HOL/Bali/WellForm.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/WellForm.thy Thu May 16 17:39:38 2013 +0200
@@ -2258,7 +2258,7 @@
qed
declare split_paired_All [simp] split_paired_Ex [simp]
setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
(* Tactical version *)
(*
@@ -2427,7 +2427,7 @@
done
declare split_paired_All [simp] split_paired_Ex [simp]
setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
lemma ty_expr_is_type:
"\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
--- a/src/HOL/Bali/WellType.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/Bali/WellType.thy Thu May 16 17:39:38 2013 +0200
@@ -494,7 +494,7 @@
declare not_None_eq [simp]
declare split_if [split] split_if_asm [split]
declare split_paired_All [simp] split_paired_Ex [simp]
-setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
+setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
lemma is_acc_class_is_accessible:
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
--- a/src/HOL/TLA/Action.thy Thu May 16 15:21:12 2013 +0200
+++ b/src/HOL/TLA/Action.thy Thu May 16 17:39:38 2013 +0200
@@ -260,7 +260,7 @@
*)
fun action_simp_tac ss intros elims =
asm_full_simp_tac
- (ss setloop ((resolve_tac ((map action_use intros)
+ (ss setloop (fn _ => (resolve_tac ((map action_use intros)
@ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
ORELSE' (eresolve_tac ((map action_use elims)
@ [conjE,disjE,exE]))));
--- a/src/Provers/splitter.ML Thu May 16 15:21:12 2013 +0200
+++ b/src/Provers/splitter.ML Thu May 16 17:39:38 2013 +0200
@@ -430,7 +430,7 @@
let
val (name, asm) = split_thm_info split
val tac = (if asm then split_asm_tac else split_tac) [split]
- in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
+ in Simplifier.addloop (ctxt, (split_name name asm, K tac)) end;
fun del_split split ctxt =
let val (name, asm) = split_thm_info split
--- a/src/Pure/raw_simplifier.ML Thu May 16 15:21:12 2013 +0200
+++ b/src/Pure/raw_simplifier.ML Thu May 16 17:39:38 2013 +0200
@@ -6,7 +6,7 @@
infix 4
addsimps delsimps addsimprocs delsimprocs
- setloop' setloop addloop addloop' delloop
+ setloop addloop delloop
setSSolver addSSolver setSolver addSolver;
signature BASIC_RAW_SIMPLIFIER =
@@ -49,10 +49,8 @@
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
@@ -821,19 +819,15 @@
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,