modifiers for classical wrappers operate on Proof.context instead of claset;
authorwenzelm
Fri Apr 12 17:21:51 2013 +0200 (2013-04-12)
changeset 51703f2e92fc0c8aa
parent 51702 dcfab8e87621
child 51704 0b0fc7dc4ce4
modifiers for classical wrappers operate on Proof.context instead of claset;
NEWS
src/Doc/IsarRef/Generic.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellForm.thy
src/HOL/HOLCF/IOA/NTP/Correctness.thy
src/HOL/HOLCF/IOA/meta_theory/TLS.thy
src/HOL/HOLCF/IOA/meta_theory/Traces.thy
src/HOL/Option.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/UNITY/Comp/Alloc.thy
src/Provers/clasimp.ML
src/Provers/classical.ML
     1.1 --- a/NEWS	Fri Apr 12 17:02:55 2013 +0200
     1.2 +++ b/NEWS	Fri Apr 12 17:21:51 2013 +0200
     1.3 @@ -129,6 +129,11 @@
     1.4  * Antiquotation @{theory_context A} is similar to @{theory A}, but
     1.5  presents the result as initial Proof.context.
     1.6  
     1.7 +* Modifiers for classical wrappers (e.g. addWrapper, delWrapper)
     1.8 +operate on Proof.context instead of claset, for uniformity with addIs,
     1.9 +addEs, addDs etc. Note that claset_of and put_claset allow to manage
    1.10 +clasets separately from the context.
    1.11 +
    1.12  
    1.13  *** System ***
    1.14  
     2.1 --- a/src/Doc/IsarRef/Generic.thy	Fri Apr 12 17:02:55 2013 +0200
     2.2 +++ b/src/Doc/IsarRef/Generic.thy	Fri Apr 12 17:21:51 2013 +0200
     2.3 @@ -1814,16 +1814,20 @@
     2.4  text {*
     2.5    \begin{mldecls}
     2.6      @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
     2.7 -    @{index_ML_op addSWrapper: "claset * (string * (Proof.context -> wrapper))
     2.8 -  -> claset"} \\
     2.9 -    @{index_ML_op addSbefore: "claset * (string * (int -> tactic)) -> claset"} \\
    2.10 -    @{index_ML_op addSafter: "claset * (string * (int -> tactic)) -> claset"} \\
    2.11 -    @{index_ML_op delSWrapper: "claset * string -> claset"} \\[0.5ex]
    2.12 -    @{index_ML_op addWrapper: "claset * (string * (Proof.context -> wrapper))
    2.13 -  -> claset"} \\
    2.14 -    @{index_ML_op addbefore: "claset * (string * (int -> tactic)) -> claset"} \\
    2.15 -    @{index_ML_op addafter: "claset * (string * (int -> tactic)) -> claset"} \\
    2.16 -    @{index_ML_op delWrapper: "claset * string -> claset"} \\[0.5ex]
    2.17 +    @{index_ML_op addSWrapper: "Proof.context *
    2.18 +  (string * (Proof.context -> wrapper)) -> Proof.context"} \\
    2.19 +    @{index_ML_op addSbefore: "Proof.context *
    2.20 +  (string * (int -> tactic)) -> Proof.context"} \\
    2.21 +    @{index_ML_op addSafter: "Proof.context *
    2.22 +  (string * (int -> tactic)) -> Proof.context"} \\
    2.23 +    @{index_ML_op delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
    2.24 +    @{index_ML_op addWrapper: "Proof.context *
    2.25 +  (string * (Proof.context -> wrapper)) -> Proof.context"} \\
    2.26 +    @{index_ML_op addbefore: "Proof.context *
    2.27 +  (string * (int -> tactic)) -> Proof.context"} \\
    2.28 +    @{index_ML_op addafter: "Proof.context *
    2.29 +  (string * (int -> tactic)) -> Proof.context"} \\
    2.30 +    @{index_ML_op delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
    2.31      @{index_ML addSss: "Proof.context -> Proof.context"} \\
    2.32      @{index_ML addss: "Proof.context -> Proof.context"} \\
    2.33    \end{mldecls}
    2.34 @@ -1856,33 +1860,33 @@
    2.35  
    2.36    \begin{description}
    2.37  
    2.38 -  \item @{text "cs addSWrapper (name, wrapper)"} adds a new wrapper,
    2.39 +  \item @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper,
    2.40    which should yield a safe tactic, to modify the existing safe step
    2.41    tactic.
    2.42  
    2.43 -  \item @{text "cs addSbefore (name, tac)"} adds the given tactic as a
    2.44 +  \item @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a
    2.45    safe wrapper, such that it is tried \emph{before} each safe step of
    2.46    the search.
    2.47  
    2.48 -  \item @{text "cs addSafter (name, tac)"} adds the given tactic as a
    2.49 +  \item @{text "ctxt addSafter (name, tac)"} adds the given tactic as a
    2.50    safe wrapper, such that it is tried when a safe step of the search
    2.51    would fail.
    2.52  
    2.53 -  \item @{text "cs delSWrapper name"} deletes the safe wrapper with
    2.54 +  \item @{text "ctxt delSWrapper name"} deletes the safe wrapper with
    2.55    the given name.
    2.56  
    2.57 -  \item @{text "cs addWrapper (name, wrapper)"} adds a new wrapper to
    2.58 +  \item @{text "ctxt addWrapper (name, wrapper)"} adds a new wrapper to
    2.59    modify the existing (unsafe) step tactic.
    2.60  
    2.61 -  \item @{text "cs addbefore (name, tac)"} adds the given tactic as an
    2.62 +  \item @{text "ctxt addbefore (name, tac)"} adds the given tactic as an
    2.63    unsafe wrapper, such that it its result is concatenated
    2.64    \emph{before} the result of each unsafe step.
    2.65  
    2.66 -  \item @{text "cs addafter (name, tac)"} adds the given tactic as an
    2.67 +  \item @{text "ctxt addafter (name, tac)"} adds the given tactic as an
    2.68    unsafe wrapper, such that it its result is concatenated \emph{after}
    2.69    the result of each unsafe step.
    2.70  
    2.71 -  \item @{text "cs delWrapper name"} deletes the unsafe wrapper with
    2.72 +  \item @{text "ctxt delWrapper name"} deletes the unsafe wrapper with
    2.73    the given name.
    2.74  
    2.75    \item @{text "addSss"} adds the simpset of the context to its
     3.1 --- a/src/HOL/Bali/AxSem.thy	Fri Apr 12 17:02:55 2013 +0200
     3.2 +++ b/src/HOL/Bali/AxSem.thy	Fri Apr 12 17:21:51 2013 +0200
     3.3 @@ -465,7 +465,7 @@
     3.4  declare split_if     [split del] split_if_asm     [split del] 
     3.5          option.split [split del] option.split_asm [split del]
     3.6  declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
     3.7 -declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
     3.8 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
     3.9  
    3.10  inductive
    3.11    ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
     4.1 --- a/src/HOL/Bali/TypeSafe.thy	Fri Apr 12 17:02:55 2013 +0200
     4.2 +++ b/src/HOL/Bali/TypeSafe.thy	Fri Apr 12 17:21:51 2013 +0200
     4.3 @@ -727,7 +727,7 @@
     4.4  declare split_if     [split del] split_if_asm     [split del] 
     4.5          option.split [split del] option.split_asm [split del]
     4.6  declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
     4.7 -declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
     4.8 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
     4.9  
    4.10  lemma FVar_lemma: 
    4.11  "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
    4.12 @@ -755,7 +755,7 @@
    4.13  declare split_paired_All [simp] split_paired_Ex [simp] 
    4.14  declare split_if     [split] split_if_asm     [split] 
    4.15          option.split [split] option.split_asm [split]
    4.16 -declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
    4.17 +setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    4.18  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    4.19  
    4.20  
    4.21 @@ -872,7 +872,7 @@
    4.22  declare split_if     [split del] split_if_asm     [split del] 
    4.23          option.split [split del] option.split_asm [split del]
    4.24  declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    4.25 -declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
    4.26 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
    4.27  
    4.28  lemma conforms_init_lvars: 
    4.29  "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
    4.30 @@ -924,7 +924,7 @@
    4.31  declare split_paired_All [simp] split_paired_Ex [simp] 
    4.32  declare split_if     [split] split_if_asm     [split] 
    4.33          option.split [split] option.split_asm [split]
    4.34 -declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
    4.35 +setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    4.36  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    4.37  
    4.38  
     5.1 --- a/src/HOL/Bali/WellForm.thy	Fri Apr 12 17:02:55 2013 +0200
     5.2 +++ b/src/HOL/Bali/WellForm.thy	Fri Apr 12 17:21:51 2013 +0200
     5.3 @@ -2128,7 +2128,7 @@
     5.4  
     5.5  declare split_paired_All [simp del] split_paired_Ex [simp del]
     5.6  declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
     5.7 -declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
     5.8 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
     5.9  
    5.10  lemma dynamic_mheadsD:   
    5.11  "\<lbrakk>emh \<in> mheads G S statT sig;    
    5.12 @@ -2257,7 +2257,7 @@
    5.13    qed
    5.14  qed
    5.15  declare split_paired_All [simp] split_paired_Ex [simp]
    5.16 -declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
    5.17 +setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    5.18  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    5.19  
    5.20  (* Tactical version *)
    5.21 @@ -2402,7 +2402,7 @@
    5.22  
    5.23  declare split_paired_All [simp del] split_paired_Ex [simp del]
    5.24  declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    5.25 -declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
    5.26 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
    5.27  
    5.28  lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
    5.29    dt=empty_dt \<longrightarrow> (case T of 
    5.30 @@ -2426,7 +2426,7 @@
    5.31      )
    5.32  done
    5.33  declare split_paired_All [simp] split_paired_Ex [simp]
    5.34 -declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
    5.35 +setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    5.36  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    5.37  
    5.38  lemma ty_expr_is_type: 
     6.1 --- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Fri Apr 12 17:02:55 2013 +0200
     6.2 +++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Fri Apr 12 17:21:51 2013 +0200
     6.3 @@ -13,10 +13,7 @@
     6.4    "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
     6.5                           else tl(sq(sen s)))"
     6.6  
     6.7 -declaration {* fn _ =>
     6.8 -  (* repeated from Traces.ML *)
     6.9 -  Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
    6.10 -*}
    6.11 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
    6.12  
    6.13  lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
    6.14    and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
     7.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Fri Apr 12 17:02:55 2013 +0200
     7.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Fri Apr 12 17:21:51 2013 +0200
     7.3 @@ -92,7 +92,7 @@
     7.4  
     7.5  lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
     7.6  
     7.7 -declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
     7.8 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
     7.9  
    7.10  
    7.11  subsection {* ex2seqC *}
     8.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Fri Apr 12 17:02:55 2013 +0200
     8.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Fri Apr 12 17:21:51 2013 +0200
     8.3 @@ -203,7 +203,7 @@
     8.4  
     8.5  lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
     8.6  declare Let_def [simp]
     8.7 -declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
     8.8 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
     8.9  
    8.10  lemmas exec_rws = executions_def is_exec_frag_def
    8.11  
     9.1 --- a/src/HOL/Option.thy	Fri Apr 12 17:02:55 2013 +0200
     9.2 +++ b/src/HOL/Option.thy	Fri Apr 12 17:21:51 2013 +0200
     9.3 @@ -46,9 +46,7 @@
     9.4  lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
     9.5    by simp
     9.6  
     9.7 -declaration {* fn _ =>
     9.8 -  Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec}))
     9.9 -*}
    9.10 +setup {* map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec})) *}
    9.11  
    9.12  lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
    9.13    by (cases xo) auto
    10.1 --- a/src/HOL/Product_Type.thy	Fri Apr 12 17:02:55 2013 +0200
    10.2 +++ b/src/HOL/Product_Type.thy	Fri Apr 12 17:21:51 2013 +0200
    10.3 @@ -428,9 +428,7 @@
    10.4    end;
    10.5  *}
    10.6  
    10.7 -declaration {* fn _ =>
    10.8 -  Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))
    10.9 -*}
   10.10 +setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
   10.11  
   10.12  lemma split_paired_All [simp, no_atp]: "(ALL x. P x) = (ALL a b. P (a, b))"
   10.13    -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
   10.14 @@ -583,9 +581,7 @@
   10.15  
   10.16  (* This prevents applications of splitE for already splitted arguments leading
   10.17     to quite time-consuming computations (in particular for nested tuples) *)
   10.18 -declaration {* fn _ =>
   10.19 -  Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
   10.20 -*}
   10.21 +setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac)) *}
   10.22  
   10.23  lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   10.24    by (rule ext) fast
    11.1 --- a/src/HOL/Set.thy	Fri Apr 12 17:02:55 2013 +0200
    11.2 +++ b/src/HOL/Set.thy	Fri Apr 12 17:21:51 2013 +0200
    11.3 @@ -379,8 +379,8 @@
    11.4    Gives better instantiation for bound:
    11.5  *}
    11.6  
    11.7 -declaration {* fn _ =>
    11.8 -  Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
    11.9 +setup {*
   11.10 +  map_theory_claset (fn ctxt => ctxt addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
   11.11  *}
   11.12  
   11.13  ML {*
    12.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Fri Apr 12 17:02:55 2013 +0200
    12.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri Apr 12 17:21:51 2013 +0200
    12.3 @@ -329,8 +329,7 @@
    12.4  ML {*
    12.5  fun record_auto_tac ctxt =
    12.6    let val ctxt' =
    12.7 -    ctxt
    12.8 -    |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
    12.9 +    (ctxt addSWrapper Record.split_wrapper)
   12.10      |> map_simpset (fn ss => ss addsimps
   12.11         [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
   12.12          @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
    13.1 --- a/src/Provers/clasimp.ML	Fri Apr 12 17:02:55 2013 +0200
    13.2 +++ b/src/Provers/clasimp.ML	Fri Apr 12 17:21:51 2013 +0200
    13.3 @@ -44,8 +44,7 @@
    13.4  
    13.5  (* simp as classical wrapper *)
    13.6  
    13.7 -fun clasimp f name tac ctxt =
    13.8 -  Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
    13.9 +fun clasimp f name tac ctxt = f (ctxt, (name, CHANGED o tac (simpset_of ctxt)));
   13.10  
   13.11  (*Add a simpset to the claset!*)
   13.12  (*Caution: only one simpset added can be added by each of addSss and addss*)
    14.1 --- a/src/Provers/classical.ML	Fri Apr 12 17:02:55 2013 +0200
    14.2 +++ b/src/Provers/classical.ML	Fri Apr 12 17:21:51 2013 +0200
    14.3 @@ -41,18 +41,18 @@
    14.4    val addSEs: Proof.context * thm list -> Proof.context
    14.5    val addSIs: Proof.context * thm list -> Proof.context
    14.6    val delrules: Proof.context * thm list -> Proof.context
    14.7 -  val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
    14.8 -  val delSWrapper: claset *  string -> claset
    14.9 -  val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
   14.10 -  val delWrapper: claset *  string -> claset
   14.11 -  val addSbefore: claset * (string * (int -> tactic)) -> claset
   14.12 -  val addSafter: claset * (string * (int -> tactic)) -> claset
   14.13 -  val addbefore: claset * (string * (int -> tactic)) -> claset
   14.14 -  val addafter: claset * (string * (int -> tactic)) -> claset
   14.15 -  val addD2: claset * (string * thm) -> claset
   14.16 -  val addE2: claset * (string * thm) -> claset
   14.17 -  val addSD2: claset * (string * thm) -> claset
   14.18 -  val addSE2: claset * (string * thm) -> claset
   14.19 +  val addSWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
   14.20 +  val delSWrapper: Proof.context * string -> Proof.context
   14.21 +  val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
   14.22 +  val delWrapper: Proof.context * string -> Proof.context
   14.23 +  val addSbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
   14.24 +  val addSafter: Proof.context * (string * (int -> tactic)) -> Proof.context
   14.25 +  val addbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
   14.26 +  val addafter: Proof.context * (string * (int -> tactic)) -> Proof.context
   14.27 +  val addD2: Proof.context * (string * thm) -> Proof.context
   14.28 +  val addE2: Proof.context * (string * thm) -> Proof.context
   14.29 +  val addSD2: Proof.context * (string * thm) -> Proof.context
   14.30 +  val addSE2: Proof.context * (string * thm) -> Proof.context
   14.31    val appSWrappers: Proof.context -> wrapper
   14.32    val appWrappers: Proof.context -> wrapper
   14.33  
   14.34 @@ -60,6 +60,8 @@
   14.35    val map_claset: (claset -> claset) -> Proof.context -> Proof.context
   14.36    val put_claset: claset -> Proof.context -> Proof.context
   14.37  
   14.38 +  val map_theory_claset: (Proof.context -> Proof.context) -> theory -> theory
   14.39 +
   14.40    val fast_tac: Proof.context -> int -> tactic
   14.41    val slow_tac: Proof.context -> int -> tactic
   14.42    val astar_tac: Proof.context -> int -> tactic
   14.43 @@ -601,6 +603,12 @@
   14.44  val get_cs = Claset.get;
   14.45  val map_cs = Claset.map;
   14.46  
   14.47 +fun map_theory_claset f thy =
   14.48 +  let
   14.49 +    val ctxt' = f (Proof_Context.init_global thy);
   14.50 +    val thy' = Proof_Context.theory_of ctxt';
   14.51 +  in Context.theory_map (Claset.map (K (claset_of ctxt'))) thy' end;
   14.52 +
   14.53  fun map_claset f = Context.proof_map (map_cs f);
   14.54  fun put_claset cs = map_claset (K cs);
   14.55  
   14.56 @@ -646,33 +654,33 @@
   14.57    else (warning msg; xs);
   14.58  
   14.59  (*Add/replace a safe wrapper*)
   14.60 -fun cs addSWrapper new_swrapper =
   14.61 -  map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
   14.62 +fun ctxt addSWrapper new_swrapper = ctxt |> map_claset
   14.63 +  (map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper));
   14.64  
   14.65  (*Add/replace an unsafe wrapper*)
   14.66 -fun cs addWrapper new_uwrapper =
   14.67 -  map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
   14.68 +fun ctxt addWrapper new_uwrapper = ctxt |> map_claset
   14.69 +  (map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper));
   14.70  
   14.71  (*Remove a safe wrapper*)
   14.72 -fun cs delSWrapper name =
   14.73 -  map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
   14.74 +fun ctxt delSWrapper name = ctxt |> map_claset
   14.75 +  (map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name));
   14.76  
   14.77  (*Remove an unsafe wrapper*)
   14.78 -fun cs delWrapper name =
   14.79 -  map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
   14.80 +fun ctxt delWrapper name = ctxt |> map_claset
   14.81 +  (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name));
   14.82  
   14.83  (* compose a safe tactic alternatively before/after safe_step_tac *)
   14.84 -fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
   14.85 -fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
   14.86 +fun ctxt addSbefore (name, tac1) = ctxt addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
   14.87 +fun ctxt addSafter (name, tac2) = ctxt addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
   14.88  
   14.89  (*compose a tactic alternatively before/after the step tactic *)
   14.90 -fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
   14.91 -fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
   14.92 +fun ctxt addbefore (name, tac1) = ctxt addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
   14.93 +fun ctxt addafter (name, tac2) = ctxt addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
   14.94  
   14.95 -fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
   14.96 -fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
   14.97 -fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   14.98 -fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   14.99 +fun ctxt addD2 (name, thm) = ctxt addafter (name, dtac thm THEN' assume_tac);
  14.100 +fun ctxt addE2 (name, thm) = ctxt addafter (name, etac thm THEN' assume_tac);
  14.101 +fun ctxt addSD2 (name, thm) = ctxt addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
  14.102 +fun ctxt addSE2 (name, thm) = ctxt addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
  14.103  
  14.104  
  14.105