# HG changeset patch
# User wenzelm
# Date 1365780111 -7200
# Node ID f2e92fc0c8aaabe50b74d850a44b28ca911782c0
# Parent  dcfab8e876215b1e1c3fc86a61ca3981721dc25f
modifiers for classical wrappers operate on Proof.context instead of claset;

diff -r dcfab8e87621 -r f2e92fc0c8aa NEWS
--- a/NEWS	Fri Apr 12 17:02:55 2013 +0200
+++ b/NEWS	Fri Apr 12 17:21:51 2013 +0200
@@ -129,6 +129,11 @@
 * Antiquotation @{theory_context A} is similar to @{theory A}, but
 presents the result as initial Proof.context.
 
+* Modifiers for classical wrappers (e.g. addWrapper, delWrapper)
+operate on Proof.context instead of claset, for uniformity with addIs,
+addEs, addDs etc. Note that claset_of and put_claset allow to manage
+clasets separately from the context.
+
 
 *** System ***
 
diff -r dcfab8e87621 -r f2e92fc0c8aa src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/Doc/IsarRef/Generic.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -1814,16 +1814,20 @@
 text {*
   \begin{mldecls}
     @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
-    @{index_ML_op addSWrapper: "claset * (string * (Proof.context -> wrapper))
-  -> claset"} \\
-    @{index_ML_op addSbefore: "claset * (string * (int -> tactic)) -> claset"} \\
-    @{index_ML_op addSafter: "claset * (string * (int -> tactic)) -> claset"} \\
-    @{index_ML_op delSWrapper: "claset * string -> claset"} \\[0.5ex]
-    @{index_ML_op addWrapper: "claset * (string * (Proof.context -> wrapper))
-  -> claset"} \\
-    @{index_ML_op addbefore: "claset * (string * (int -> tactic)) -> claset"} \\
-    @{index_ML_op addafter: "claset * (string * (int -> tactic)) -> claset"} \\
-    @{index_ML_op delWrapper: "claset * string -> claset"} \\[0.5ex]
+    @{index_ML_op addSWrapper: "Proof.context *
+  (string * (Proof.context -> wrapper)) -> Proof.context"} \\
+    @{index_ML_op addSbefore: "Proof.context *
+  (string * (int -> tactic)) -> Proof.context"} \\
+    @{index_ML_op addSafter: "Proof.context *
+  (string * (int -> tactic)) -> Proof.context"} \\
+    @{index_ML_op delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
+    @{index_ML_op addWrapper: "Proof.context *
+  (string * (Proof.context -> wrapper)) -> Proof.context"} \\
+    @{index_ML_op addbefore: "Proof.context *
+  (string * (int -> tactic)) -> Proof.context"} \\
+    @{index_ML_op addafter: "Proof.context *
+  (string * (int -> tactic)) -> Proof.context"} \\
+    @{index_ML_op delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
     @{index_ML addSss: "Proof.context -> Proof.context"} \\
     @{index_ML addss: "Proof.context -> Proof.context"} \\
   \end{mldecls}
@@ -1856,33 +1860,33 @@
 
   \begin{description}
 
-  \item @{text "cs addSWrapper (name, wrapper)"} adds a new wrapper,
+  \item @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper,
   which should yield a safe tactic, to modify the existing safe step
   tactic.
 
-  \item @{text "cs addSbefore (name, tac)"} adds the given tactic as a
+  \item @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a
   safe wrapper, such that it is tried \emph{before} each safe step of
   the search.
 
-  \item @{text "cs addSafter (name, tac)"} adds the given tactic as a
+  \item @{text "ctxt addSafter (name, tac)"} adds the given tactic as a
   safe wrapper, such that it is tried when a safe step of the search
   would fail.
 
-  \item @{text "cs delSWrapper name"} deletes the safe wrapper with
+  \item @{text "ctxt delSWrapper name"} deletes the safe wrapper with
   the given name.
 
-  \item @{text "cs addWrapper (name, wrapper)"} adds a new wrapper to
+  \item @{text "ctxt addWrapper (name, wrapper)"} adds a new wrapper to
   modify the existing (unsafe) step tactic.
 
-  \item @{text "cs addbefore (name, tac)"} adds the given tactic as an
+  \item @{text "ctxt addbefore (name, tac)"} adds the given tactic as an
   unsafe wrapper, such that it its result is concatenated
   \emph{before} the result of each unsafe step.
 
-  \item @{text "cs addafter (name, tac)"} adds the given tactic as an
+  \item @{text "ctxt addafter (name, tac)"} adds the given tactic as an
   unsafe wrapper, such that it its result is concatenated \emph{after}
   the result of each unsafe step.
 
-  \item @{text "cs delWrapper name"} deletes the unsafe wrapper with
+  \item @{text "ctxt delWrapper name"} deletes the unsafe wrapper with
   the given name.
 
   \item @{text "addSss"} adds the simpset of the context to its
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Bali/AxSem.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -465,7 +465,7 @@
 declare split_if     [split del] split_if_asm     [split del] 
         option.split [split del] option.split_asm [split del]
 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
 
 inductive
   ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -727,7 +727,7 @@
 declare split_if     [split del] split_if_asm     [split del] 
         option.split [split del] option.split_asm [split del]
 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
 
 lemma FVar_lemma: 
 "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
@@ -755,7 +755,7 @@
 declare split_paired_All [simp] split_paired_Ex [simp] 
 declare split_if     [split] split_if_asm     [split] 
         option.split [split] option.split_asm [split]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 
@@ -872,7 +872,7 @@
 declare split_if     [split del] split_if_asm     [split del] 
         option.split [split del] option.split_asm [split del]
 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
 
 lemma conforms_init_lvars: 
 "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
@@ -924,7 +924,7 @@
 declare split_paired_All [simp] split_paired_Ex [simp] 
 declare split_if     [split] split_if_asm     [split] 
         option.split [split] option.split_asm [split]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Bali/WellForm.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -2128,7 +2128,7 @@
 
 declare split_paired_All [simp del] split_paired_Ex [simp del]
 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
 
 lemma dynamic_mheadsD:   
 "\<lbrakk>emh \<in> mheads G S statT sig;    
@@ -2257,7 +2257,7 @@
   qed
 qed
 declare split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 (* Tactical version *)
@@ -2402,7 +2402,7 @@
 
 declare split_paired_All [simp del] split_paired_Ex [simp del]
 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
 
 lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
   dt=empty_dt \<longrightarrow> (case T of 
@@ -2426,7 +2426,7 @@
     )
 done
 declare split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
 
 lemma ty_expr_is_type: 
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/HOLCF/IOA/NTP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -13,10 +13,7 @@
   "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
                          else tl(sq(sen s)))"
 
-declaration {* fn _ =>
-  (* repeated from Traces.ML *)
-  Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
-*}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
 
 lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
   and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -92,7 +92,7 @@
 
 lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
 
-declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
 
 
 subsection {* ex2seqC *}
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -203,7 +203,7 @@
 
 lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
 declare Let_def [simp]
-declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
 
 lemmas exec_rws = executions_def is_exec_frag_def
 
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Option.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -46,9 +46,7 @@
 lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
   by simp
 
-declaration {* fn _ =>
-  Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec}))
-*}
+setup {* map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec})) *}
 
 lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
   by (cases xo) auto
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Product_Type.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -428,9 +428,7 @@
   end;
 *}
 
-declaration {* fn _ =>
-  Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))
-*}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
 
 lemma split_paired_All [simp, no_atp]: "(ALL x. P x) = (ALL a b. P (a, b))"
   -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
@@ -583,9 +581,7 @@
 
 (* This prevents applications of splitE for already splitted arguments leading
    to quite time-consuming computations (in particular for nested tuples) *)
-declaration {* fn _ =>
-  Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
-*}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac)) *}
 
 lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
   by (rule ext) fast
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Set.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -379,8 +379,8 @@
   Gives better instantiation for bound:
 *}
 
-declaration {* fn _ =>
-  Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
+setup {*
+  map_theory_claset (fn ctxt => ctxt addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
 *}
 
 ML {*
diff -r dcfab8e87621 -r f2e92fc0c8aa src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri Apr 12 17:21:51 2013 +0200
@@ -329,8 +329,7 @@
 ML {*
 fun record_auto_tac ctxt =
   let val ctxt' =
-    ctxt
-    |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
+    (ctxt addSWrapper Record.split_wrapper)
     |> map_simpset (fn ss => ss addsimps
        [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
         @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
diff -r dcfab8e87621 -r f2e92fc0c8aa src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/Provers/clasimp.ML	Fri Apr 12 17:21:51 2013 +0200
@@ -44,8 +44,7 @@
 
 (* simp as classical wrapper *)
 
-fun clasimp f name tac ctxt =
-  Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
+fun clasimp f name tac ctxt = f (ctxt, (name, CHANGED o tac (simpset_of ctxt)));
 
 (*Add a simpset to the claset!*)
 (*Caution: only one simpset added can be added by each of addSss and addss*)
diff -r dcfab8e87621 -r f2e92fc0c8aa src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Apr 12 17:02:55 2013 +0200
+++ b/src/Provers/classical.ML	Fri Apr 12 17:21:51 2013 +0200
@@ -41,18 +41,18 @@
   val addSEs: Proof.context * thm list -> Proof.context
   val addSIs: Proof.context * thm list -> Proof.context
   val delrules: Proof.context * thm list -> Proof.context
-  val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
-  val delSWrapper: claset *  string -> claset
-  val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
-  val delWrapper: claset *  string -> claset
-  val addSbefore: claset * (string * (int -> tactic)) -> claset
-  val addSafter: claset * (string * (int -> tactic)) -> claset
-  val addbefore: claset * (string * (int -> tactic)) -> claset
-  val addafter: claset * (string * (int -> tactic)) -> claset
-  val addD2: claset * (string * thm) -> claset
-  val addE2: claset * (string * thm) -> claset
-  val addSD2: claset * (string * thm) -> claset
-  val addSE2: claset * (string * thm) -> claset
+  val addSWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
+  val delSWrapper: Proof.context * string -> Proof.context
+  val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
+  val delWrapper: Proof.context * string -> Proof.context
+  val addSbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
+  val addSafter: Proof.context * (string * (int -> tactic)) -> Proof.context
+  val addbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
+  val addafter: Proof.context * (string * (int -> tactic)) -> Proof.context
+  val addD2: Proof.context * (string * thm) -> Proof.context
+  val addE2: Proof.context * (string * thm) -> Proof.context
+  val addSD2: Proof.context * (string * thm) -> Proof.context
+  val addSE2: Proof.context * (string * thm) -> Proof.context
   val appSWrappers: Proof.context -> wrapper
   val appWrappers: Proof.context -> wrapper
 
@@ -60,6 +60,8 @@
   val map_claset: (claset -> claset) -> Proof.context -> Proof.context
   val put_claset: claset -> Proof.context -> Proof.context
 
+  val map_theory_claset: (Proof.context -> Proof.context) -> theory -> theory
+
   val fast_tac: Proof.context -> int -> tactic
   val slow_tac: Proof.context -> int -> tactic
   val astar_tac: Proof.context -> int -> tactic
@@ -601,6 +603,12 @@
 val get_cs = Claset.get;
 val map_cs = Claset.map;
 
+fun map_theory_claset f thy =
+  let
+    val ctxt' = f (Proof_Context.init_global thy);
+    val thy' = Proof_Context.theory_of ctxt';
+  in Context.theory_map (Claset.map (K (claset_of ctxt'))) thy' end;
+
 fun map_claset f = Context.proof_map (map_cs f);
 fun put_claset cs = map_claset (K cs);
 
@@ -646,33 +654,33 @@
   else (warning msg; xs);
 
 (*Add/replace a safe wrapper*)
-fun cs addSWrapper new_swrapper =
-  map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
+fun ctxt addSWrapper new_swrapper = ctxt |> map_claset
+  (map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper));
 
 (*Add/replace an unsafe wrapper*)
-fun cs addWrapper new_uwrapper =
-  map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
+fun ctxt addWrapper new_uwrapper = ctxt |> map_claset
+  (map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper));
 
 (*Remove a safe wrapper*)
-fun cs delSWrapper name =
-  map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
+fun ctxt delSWrapper name = ctxt |> map_claset
+  (map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name));
 
 (*Remove an unsafe wrapper*)
-fun cs delWrapper name =
-  map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
+fun ctxt delWrapper name = ctxt |> map_claset
+  (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name));
 
 (* compose a safe tactic alternatively before/after safe_step_tac *)
-fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
-fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
+fun ctxt addSbefore (name, tac1) = ctxt addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
+fun ctxt addSafter (name, tac2) = ctxt addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
 
 (*compose a tactic alternatively before/after the step tactic *)
-fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
-fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
+fun ctxt addbefore (name, tac1) = ctxt addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
+fun ctxt addafter (name, tac2) = ctxt addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
 
-fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
-fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
-fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
-fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
+fun ctxt addD2 (name, thm) = ctxt addafter (name, dtac thm THEN' assume_tac);
+fun ctxt addE2 (name, thm) = ctxt addafter (name, etac thm THEN' assume_tac);
+fun ctxt addSD2 (name, thm) = ctxt addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
+fun ctxt addSE2 (name, thm) = ctxt addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);