proper context for assume_tac (atac remains as fall-back without context);
authorwenzelm
Mon, 10 Nov 2014 21:49:48 +0100
changeset 58963 26bf09b95dda
parent 58960 4bee6d8c1500
child 58964 a93d114eaa5d
proper context for assume_tac (atac remains as fall-back without context);
NEWS
src/CCL/Wfd.thy
src/CTT/Arith.thy
src/CTT/Bool.thy
src/CTT/CTT.thy
src/CTT/ex/Elimination.thy
src/CTT/ex/Equality.thy
src/CTT/ex/Synthesis.thy
src/CTT/ex/Typechecking.thy
src/CTT/rew.ML
src/Doc/Implementation/Tactic.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/Tutorial/Protocol/Event.thy
src/FOL/IFOL.thy
src/FOL/intprover.ML
src/FOL/simpdata.ML
src/FOLP/IFOLP.thy
src/FOLP/classical.ML
src/FOLP/ex/Intuitionistic.thy
src/FOLP/ex/Propositional_Int.thy
src/FOLP/ex/Quantifiers_Int.thy
src/FOLP/intprover.ML
src/FOLP/simp.ML
src/HOL/Auth/Event.thy
src/HOL/Auth/Recur.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Table.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOL.thy
src/HOL/HOLCF/FOCUS/Buffer_adm.thy
src/HOL/Hoare_Parallel/Gar_Coll.thy
src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
src/HOL/IMPP/Hoare.thy
src/HOL/IMPP/Misc.thy
src/HOL/IMPP/Natural.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/NanoJava/Example.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SET_Protocol/Cardholder_Registration.thy
src/HOL/SET_Protocol/Event_SET.thy
src/HOL/SET_Protocol/Purchase.thy
src/HOL/Set.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/function_elims.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/Transfer/transfer_bnf.ML
src/HOL/Tools/cnf.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record.ML
src/HOL/Tools/set_comprehension_pointfree.ML
src/HOL/Tools/simpdata.ML
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY_tactics.ML
src/HOL/Word/Word.thy
src/HOL/ex/Meson_Test.thy
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/typedsimp.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/method.ML
src/Pure/Tools/rule_insts.ML
src/Pure/goal.ML
src/Pure/simplifier.ML
src/Pure/tactic.ML
src/Sequents/simpdata.ML
src/Tools/intuitionistic.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/typechk.ML
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/SubstAx.thy
--- a/NEWS	Sun Nov 09 20:49:28 2014 +0100
+++ b/NEWS	Mon Nov 10 21:49:48 2014 +0100
@@ -190,8 +190,9 @@
 
 *** ML ***
 
-* Proper context for various elementary tactics: match_tac, compose_tac,
-Splitter.split_tac etc.  Minor INCOMPATIBILITY.
+* Proper context for various elementary tactics: assume_tac,
+match_tac, compose_tac, Splitter.split_tac etc.  Minor
+INCOMPATIBILITY.
 
 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
 PARALLEL_GOALS.
--- a/src/CCL/Wfd.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CCL/Wfd.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -48,7 +48,7 @@
 
 ML {*
   fun wfd_strengthen_tac ctxt s i =
-    res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
+    res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1)
 *}
 
 lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
--- a/src/CTT/Arith.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CTT/Arith.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -54,12 +54,12 @@
 
 lemma add_typing: "[| a:N;  b:N |] ==> a #+ b : N"
 apply (unfold arith_defs)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 lemma add_typingL: "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
 apply (unfold arith_defs)
-apply (tactic "equal_tac []")
+apply (tactic "equal_tac @{context} []")
 done
 
 
@@ -67,12 +67,12 @@
 
 lemma addC0: "b:N ==> 0 #+ b = b : N"
 apply (unfold arith_defs)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 lemma addC_succ: "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
 apply (unfold arith_defs)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 
@@ -82,24 +82,24 @@
 
 lemma mult_typing: "[| a:N;  b:N |] ==> a #* b : N"
 apply (unfold arith_defs)
-apply (tactic {* typechk_tac [@{thm add_typing}] *})
+apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *})
 done
 
 lemma mult_typingL: "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
 apply (unfold arith_defs)
-apply (tactic {* equal_tac [@{thm add_typingL}] *})
+apply (tactic {* equal_tac @{context} [@{thm add_typingL}] *})
 done
 
 (*computation for mult: 0 and successor cases*)
 
 lemma multC0: "b:N ==> 0 #* b = 0 : N"
 apply (unfold arith_defs)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 lemma multC_succ: "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
 apply (unfold arith_defs)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 
@@ -109,12 +109,12 @@
 
 lemma diff_typing: "[| a:N;  b:N |] ==> a - b : N"
 apply (unfold arith_defs)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 lemma diff_typingL: "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
 apply (unfold arith_defs)
-apply (tactic "equal_tac []")
+apply (tactic "equal_tac @{context} []")
 done
 
 
@@ -122,7 +122,7 @@
 
 lemma diffC0: "a:N ==> a - 0 = a : N"
 apply (unfold arith_defs)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 (*Note: rec(a, 0, %z w.z) is pred(a). *)
@@ -130,7 +130,7 @@
 lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
 apply (unfold arith_defs)
 apply (tactic {* NE_tac @{context} "b" 1 *})
-apply (tactic "hyp_rew_tac []")
+apply (tactic "hyp_rew_tac @{context} []")
 done
 
 
@@ -138,9 +138,9 @@
   succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
 lemma diff_succ_succ: "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
 apply (unfold arith_defs)
-apply (tactic "hyp_rew_tac []")
+apply (tactic "hyp_rew_tac @{context} []")
 apply (tactic {* NE_tac @{context} "b" 1 *})
-apply (tactic "hyp_rew_tac []")
+apply (tactic "hyp_rew_tac @{context} []")
 done
 
 
@@ -173,11 +173,11 @@
 
 local val congr_rls = @{thms congr_rls} in
 
-fun arith_rew_tac prems = make_rew_tac
-    (Arith_simp.norm_tac(congr_rls, prems))
+fun arith_rew_tac ctxt prems = make_rew_tac ctxt
+    (Arith_simp.norm_tac ctxt (congr_rls, prems))
 
-fun hyp_arith_rew_tac prems = make_rew_tac
-    (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems))
+fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt
+    (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems))
 
 end
 *}
@@ -188,7 +188,7 @@
 (*Associative law for addition*)
 lemma add_assoc: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_arith_rew_tac []")
+apply (tactic "hyp_arith_rew_tac @{context} []")
 done
 
 
@@ -196,11 +196,11 @@
   Must simplify after first induction!  Orientation of rewrites is delicate*)
 lemma add_commute: "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_arith_rew_tac []")
+apply (tactic "hyp_arith_rew_tac @{context} []")
 apply (tactic {* NE_tac @{context} "b" 2 *})
 apply (rule sym_elem)
 apply (tactic {* NE_tac @{context} "b" 1 *})
-apply (tactic "hyp_arith_rew_tac []")
+apply (tactic "hyp_arith_rew_tac @{context} []")
 done
 
 
@@ -209,32 +209,32 @@
 (*right annihilation in product*)
 lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_arith_rew_tac []")
+apply (tactic "hyp_arith_rew_tac @{context} []")
 done
 
 (*right successor law for multiplication*)
 lemma mult_succ_right: "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
+apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *})
 apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
 done
 
 (*Commutative law for multiplication*)
 lemma mult_commute: "[| a:N;  b:N |] ==> a #* b = b #* a : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [@{thm mult_0_right}, @{thm mult_succ_right}] *})
+apply (tactic {* hyp_arith_rew_tac @{context} [@{thm mult_0_right}, @{thm mult_succ_right}] *})
 done
 
 (*addition distributes over multiplication*)
 lemma add_mult_distrib: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
+apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *})
 done
 
 (*Associative law for multiplication*)
 lemma mult_assoc: "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* hyp_arith_rew_tac [@{thm add_mult_distrib}] *})
+apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_mult_distrib}] *})
 done
 
 
@@ -246,7 +246,7 @@
 
 lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_arith_rew_tac []")
+apply (tactic "hyp_arith_rew_tac @{context} []")
 done
 
 
@@ -263,15 +263,15 @@
 apply (rule_tac [3] intr_rls)
 (*case analysis on x in
     (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
-apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac 4")
+apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac @{context} 4")
 (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
 apply (rule_tac [5] replace_type)
 apply (rule_tac [4] replace_type)
-apply (tactic "arith_rew_tac []")
+apply (tactic "arith_rew_tac @{context} []")
 (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   Both follow by rewriting, (2) using quantified induction hyp*)
-apply (tactic "intr_tac []") (*strips remaining PRODs*)
-apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
+apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*)
+apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *})
 apply assumption
 done
 
@@ -293,46 +293,46 @@
 
 lemma absdiff_typing: "[| a:N;  b:N |] ==> a |-| b : N"
 apply (unfold arith_defs)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 lemma absdiff_typingL: "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
 apply (unfold arith_defs)
-apply (tactic "equal_tac []")
+apply (tactic "equal_tac @{context} []")
 done
 
 lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
 apply (unfold absdiff_def)
-apply (tactic {* arith_rew_tac [@{thm diff_self_eq_0}] *})
+apply (tactic {* arith_rew_tac @{context} [@{thm diff_self_eq_0}] *})
 done
 
 lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
 apply (unfold absdiff_def)
-apply (tactic "hyp_arith_rew_tac []")
+apply (tactic "hyp_arith_rew_tac @{context} []")
 done
 
 
 lemma absdiff_succ_succ: "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
 apply (unfold absdiff_def)
-apply (tactic "hyp_arith_rew_tac []")
+apply (tactic "hyp_arith_rew_tac @{context} []")
 done
 
 (*Note how easy using commutative laws can be?  ...not always... *)
 lemma absdiff_commute: "[| a:N;  b:N |] ==> a |-| b = b |-| a : N"
 apply (unfold absdiff_def)
 apply (rule add_commute)
-apply (tactic {* typechk_tac [@{thm diff_typing}] *})
+apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *})
 done
 
 (*If a+b=0 then a=0.   Surprisingly tedious*)
 schematic_lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
 apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (rule_tac [3] replace_type)
-apply (tactic "arith_rew_tac []")
-apply (tactic "intr_tac []") (*strips remaining PRODs*)
+apply (tactic "arith_rew_tac @{context} []")
+apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*)
 apply (rule_tac [2] zero_ne_succ [THEN FE])
 apply (erule_tac [3] EqE [THEN sym_elem])
-apply (tactic {* typechk_tac [@{thm add_typing}] *})
+apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *})
 done
 
 (*Version of above with the premise  a+b=0.
@@ -341,7 +341,7 @@
 apply (rule EqE)
 apply (rule add_eq0_lemma [THEN ProdE])
 apply (rule_tac [3] EqI)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
@@ -349,12 +349,12 @@
     "[| a:N;  b:N;  a |-| b = 0 : N |] ==>
      ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
 apply (unfold absdiff_def)
-apply (tactic "intr_tac []")
-apply (tactic eqintr_tac)
+apply (tactic "intr_tac @{context} []")
+apply (tactic "eqintr_tac @{context}")
 apply (rule_tac [2] add_eq0)
 apply (rule add_eq0)
 apply (rule_tac [6] add_commute [THEN trans_elem])
-apply (tactic {* typechk_tac [@{thm diff_typing}] *})
+apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *})
 done
 
 (*if  a |-| b = 0  then  a = b
@@ -362,11 +362,11 @@
 lemma absdiff_eq0: "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N"
 apply (rule EqE)
 apply (rule absdiff_eq0_lem [THEN SumE])
-apply (tactic "TRYALL assume_tac")
-apply (tactic eqintr_tac)
+apply (tactic "TRYALL (assume_tac @{context})")
+apply (tactic "eqintr_tac @{context}")
 apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
-apply (rule_tac [3] EqE, tactic "assume_tac 3")
-apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
+apply (rule_tac [3] EqE, tactic "assume_tac @{context} 3")
+apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *})
 done
 
 
@@ -376,12 +376,12 @@
 
 lemma mod_typing: "[| a:N;  b:N |] ==> a mod b : N"
 apply (unfold mod_def)
-apply (tactic {* typechk_tac [@{thm absdiff_typing}] *})
+apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}] *})
 done
 
 lemma mod_typingL: "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
 apply (unfold mod_def)
-apply (tactic {* equal_tac [@{thm absdiff_typingL}] *})
+apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}] *})
 done
 
 
@@ -389,13 +389,13 @@
 
 lemma modC0: "b:N ==> 0 mod b = 0 : N"
 apply (unfold mod_def)
-apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
+apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *})
 done
 
 lemma modC_succ:
 "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
 apply (unfold mod_def)
-apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
+apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *})
 done
 
 
@@ -403,12 +403,12 @@
 
 lemma div_typing: "[| a:N;  b:N |] ==> a div b : N"
 apply (unfold div_def)
-apply (tactic {* typechk_tac [@{thm absdiff_typing}, @{thm mod_typing}] *})
+apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}, @{thm mod_typing}] *})
 done
 
 lemma div_typingL: "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
 apply (unfold div_def)
-apply (tactic {* equal_tac [@{thm absdiff_typingL}, @{thm mod_typingL}] *})
+apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}, @{thm mod_typingL}] *})
 done
 
 lemmas div_typing_rls = mod_typing div_typing absdiff_typing
@@ -418,14 +418,14 @@
 
 lemma divC0: "b:N ==> 0 div b = 0 : N"
 apply (unfold div_def)
-apply (tactic {* rew_tac [@{thm mod_typing}, @{thm absdiff_typing}] *})
+apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm absdiff_typing}] *})
 done
 
 lemma divC_succ:
  "[| a:N;  b:N |] ==> succ(a) div b =
      rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
 apply (unfold div_def)
-apply (tactic {* rew_tac [@{thm mod_typing}] *})
+apply (tactic {* rew_tac @{context} [@{thm mod_typing}] *})
 done
 
 
@@ -433,9 +433,9 @@
 lemma divC_succ2: "[| a:N;  b:N |] ==>
      succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
 apply (rule divC_succ [THEN trans_elem])
-apply (tactic {* rew_tac (@{thms div_typing_rls} @ [@{thm modC_succ}]) *})
+apply (tactic {* rew_tac @{context} (@{thms div_typing_rls} @ [@{thm modC_succ}]) *})
 apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
-apply (tactic {* rew_tac [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *})
+apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *})
 done
 
 (*for case analysis on whether a number is 0 or a successor*)
@@ -444,26 +444,26 @@
 apply (tactic {* NE_tac @{context} "a" 1 *})
 apply (rule_tac [3] PlusI_inr)
 apply (rule_tac [2] PlusI_inl)
-apply (tactic eqintr_tac)
-apply (tactic "equal_tac []")
+apply (tactic "eqintr_tac @{context}")
+apply (tactic "equal_tac @{context} []")
 done
 
 (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
 lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic {* arith_rew_tac (@{thms div_typing_rls} @
+apply (tactic {* arith_rew_tac @{context} (@{thms div_typing_rls} @
   [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
 apply (rule EqE)
 (*case analysis on   succ(u mod b)|-|b  *)
 apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
 apply (erule_tac [3] SumE)
-apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @
+apply (tactic {* hyp_arith_rew_tac @{context} (@{thms div_typing_rls} @
   [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
 (*Replace one occurrence of  b  by succ(u mod b).  Clumsy!*)
 apply (rule add_typingL [THEN trans_elem])
 apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
 apply (rule_tac [3] refl_elem)
-apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *})
+apply (tactic {* hyp_arith_rew_tac @{context} @{thms div_typing_rls} *})
 done
 
 end
--- a/src/CTT/Bool.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CTT/Bool.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -33,7 +33,7 @@
 (*formation rule*)
 lemma boolF: "Bool type"
 apply (unfold bool_defs)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 
@@ -41,21 +41,21 @@
 
 lemma boolI_true: "true : Bool"
 apply (unfold bool_defs)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 lemma boolI_false: "false : Bool"
 apply (unfold bool_defs)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 (*elimination rule: typing of cond*)
 lemma boolE: 
     "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
 apply (unfold bool_defs)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 apply (erule_tac [!] TE)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 lemma boolEL: 
@@ -72,18 +72,18 @@
     "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
 apply (unfold bool_defs)
 apply (rule comp_rls)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 apply (erule_tac [!] TE)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 lemma boolC_false: 
     "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
 apply (unfold bool_defs)
 apply (rule comp_rls)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 apply (erule_tac [!] TE)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 end
--- a/src/CTT/CTT.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CTT/CTT.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -336,11 +336,11 @@
 in
 
 (*Try solving a:A or a=b:A by assumption provided a is rigid!*)
-val test_assume_tac = SUBGOAL(fn (prem,i) =>
+fun test_assume_tac ctxt = SUBGOAL(fn (prem,i) =>
     if is_rigid_elem (Logic.strip_assums_concl prem)
-    then  assume_tac i  else  no_tac)
+    then  assume_tac ctxt i  else  no_tac)
 
-fun ASSUME tf i = test_assume_tac i  ORELSE  tf i
+fun ASSUME ctxt tf i = test_assume_tac ctxt i  ORELSE  tf i
 
 end;
 
@@ -356,26 +356,26 @@
     @{thms elimL_rls} @ @{thms refl_elem}
 in
 
-fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
+fun routine_tac rls ctxt prems = ASSUME ctxt (filt_resolve_tac (prems @ rls) 4);
 
 (*Solve all subgoals "A type" using formation rules. *)
-val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac @{thms form_rls} 1));
+fun form_tac ctxt = REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac @{thms form_rls} 1));
 
 (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
-fun typechk_tac thms =
+fun typechk_tac ctxt thms =
   let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3
-  in  REPEAT_FIRST (ASSUME tac)  end
+  in  REPEAT_FIRST (ASSUME ctxt tac)  end
 
 (*Solve a:A (a flexible, A rigid) by introduction rules.
   Cannot use stringtrees (filt_resolve_tac) since
   goals like ?a:SUM(A,B) have a trivial head-string *)
-fun intr_tac thms =
+fun intr_tac ctxt thms =
   let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1
-  in  REPEAT_FIRST (ASSUME tac)  end
+  in  REPEAT_FIRST (ASSUME ctxt tac)  end
 
 (*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
-fun equal_tac thms =
-  REPEAT_FIRST (ASSUME (filt_resolve_tac (thms @ equal_rls) 3))
+fun equal_tac ctxt thms =
+  REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (thms @ equal_rls) 3))
 
 end
 
@@ -408,7 +408,8 @@
 ML {*
 (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
   Uses other intro rules to avoid changing flexible goals.*)
-val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
+fun eqintr_tac ctxt =
+  REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
 
 (** Tactics that instantiate CTT-rules.
     Vars in the given terms will be incremented!
@@ -426,11 +427,11 @@
 (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
 
 (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
-fun add_mp_tac i =
-    rtac @{thm subst_prodE} i  THEN  assume_tac i  THEN  assume_tac i
+fun add_mp_tac ctxt i =
+    rtac @{thm subst_prodE} i  THEN  assume_tac ctxt i  THEN  assume_tac ctxt i
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = etac @{thm subst_prodE} i  THEN  assume_tac i
+fun mp_tac ctxt i = etac @{thm subst_prodE} i  THEN  assume_tac ctxt i
 
 (*"safe" when regarded as predicate calculus rules*)
 val safe_brls = sort (make_ord lessb)
@@ -445,18 +446,18 @@
 val (safe0_brls, safep_brls) =
     List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls
 
-fun safestep_tac thms i =
-    form_tac  ORELSE
+fun safestep_tac ctxt thms i =
+    form_tac ctxt ORELSE
     resolve_tac thms i  ORELSE
-    biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
+    biresolve_tac safe0_brls i  ORELSE  mp_tac ctxt i  ORELSE
     DETERM (biresolve_tac safep_brls i)
 
-fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i)
+fun safe_tac ctxt thms i = DEPTH_SOLVE_1 (safestep_tac ctxt thms i)
 
-fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls
+fun step_tac ctxt thms = safestep_tac ctxt thms  ORELSE'  biresolve_tac unsafe_brls
 
 (*Fails unless it solves the goal!*)
-fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
+fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms)
 *}
 
 ML_file "rew.ML"
@@ -479,7 +480,7 @@
   apply (unfold basic_defs)
   apply (rule major [THEN SumE])
   apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
-  apply (tactic {* typechk_tac @{thms assms} *})
+  apply (tactic {* typechk_tac @{context} @{thms assms} *})
   done
 
 end
--- a/src/CTT/ex/Elimination.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CTT/ex/Elimination.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -15,36 +15,36 @@
 text "This finds the functions fst and snd!"
 
 schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
-apply (tactic {* pc_tac [] 1 *})
+apply (tactic {* pc_tac @{context} [] 1 *})
 done
 
 schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
-apply (tactic {* pc_tac [] 1 *})
+apply (tactic {* pc_tac @{context} [] 1 *})
 back
 done
 
 text "Double negation of the Excluded Middle"
 schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
-apply (tactic "intr_tac []")
+apply (tactic "intr_tac @{context} []")
 apply (rule ProdE)
 apply assumption
-apply (tactic "pc_tac [] 1")
+apply (tactic "pc_tac @{context} [] 1")
 done
 
 schematic_lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
-apply (tactic "pc_tac [] 1")
+apply (tactic "pc_tac @{context} [] 1")
 done
 (*The sequent version (ITT) could produce an interesting alternative
   by backtracking.  No longer.*)
 
 text "Binary sums and products"
 schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
-apply (tactic "pc_tac [] 1")
+apply (tactic "pc_tac @{context} [] 1")
 done
 
 (*A distributive law*)
 schematic_lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
-apply (tactic "pc_tac [] 1")
+apply (tactic "pc_tac @{context} [] 1")
 done
 
 (*more general version, same proof*)
@@ -53,12 +53,12 @@
     and "!!x. x:A ==> B(x) type"
     and "!!x. x:A ==> C(x) type"
   shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
-apply (tactic {* pc_tac @{thms assms} 1 *})
+apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
 done
 
 text "Construction of the currying functional"
 schematic_lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
-apply (tactic "pc_tac [] 1")
+apply (tactic "pc_tac @{context} [] 1")
 done
 
 (*more general goal with same proof*)
@@ -68,12 +68,12 @@
     and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
   shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
                       (PROD x:A . PROD y:B(x) . C(<x,y>))"
-apply (tactic {* pc_tac @{thms assms} 1 *})
+apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
 done
 
 text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
 schematic_lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
-apply (tactic "pc_tac [] 1")
+apply (tactic "pc_tac @{context} [] 1")
 done
 
 (*more general goal with same proof*)
@@ -83,12 +83,12 @@
     and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
   shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
         --> (PROD z : (SUM x:A . B(x)) . C(z))"
-apply (tactic {* pc_tac @{thms assms} 1 *})
+apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
 done
 
 text "Function application"
 schematic_lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
-apply (tactic "pc_tac [] 1")
+apply (tactic "pc_tac @{context} [] 1")
 done
 
 text "Basic test of quantifier reasoning"
@@ -99,7 +99,7 @@
   shows
     "?a :     (SUM y:B . PROD x:A . C(x,y))
           --> (PROD x:A . SUM y:B . C(x,y))"
-apply (tactic {* pc_tac @{thms assms} 1 *})
+apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
 done
 
 text "Martin-Lof (1984) pages 36-7: the combinator S"
@@ -109,7 +109,7 @@
     and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
   shows "?a :    (PROD x:A. PROD y:B(x). C(x,y))
              --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* pc_tac @{thms assms} 1 *})
+apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
 done
 
 text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
@@ -119,13 +119,13 @@
     and "!!z. z: A+B ==> C(z) type"
   shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
           --> (PROD z: A+B. C(z))"
-apply (tactic {* pc_tac @{thms assms} 1 *})
+apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
 done
 
 (*towards AXIOM OF CHOICE*)
 schematic_lemma [folded basic_defs]:
   "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
-apply (tactic "pc_tac [] 1")
+apply (tactic "pc_tac @{context} [] 1")
 done
 
 
@@ -137,15 +137,15 @@
     and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
   shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
                          (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* intr_tac @{thms assms} *})
-apply (tactic "add_mp_tac 2")
-apply (tactic "add_mp_tac 1")
+apply (tactic {* intr_tac @{context} @{thms assms} *})
+apply (tactic "add_mp_tac @{context} 2")
+apply (tactic "add_mp_tac @{context} 1")
 apply (erule SumE_fst)
 apply (rule replace_type)
 apply (rule subst_eqtyparg)
 apply (rule comp_rls)
 apply (rule_tac [4] SumE_snd)
-apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms assms}) *})
+apply (tactic {* typechk_tac @{context} (@{thm SumE_fst} :: @{thms assms}) *})
 done
 
 text "Axiom of choice.  Proof without fst, snd.  Harder still!"
@@ -155,19 +155,19 @@
     and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
   shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
                          (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
-apply (tactic {* intr_tac @{thms assms} *})
+apply (tactic {* intr_tac @{context} @{thms assms} *})
 (*Must not use add_mp_tac as subst_prodE hides the construction.*)
 apply (rule ProdE [THEN SumE], assumption)
-apply (tactic "TRYALL assume_tac")
+apply (tactic "TRYALL (assume_tac @{context})")
 apply (rule replace_type)
 apply (rule subst_eqtyparg)
 apply (rule comp_rls)
 apply (erule_tac [4] ProdE [THEN SumE])
-apply (tactic {* typechk_tac @{thms assms} *})
+apply (tactic {* typechk_tac @{context} @{thms assms} *})
 apply (rule replace_type)
 apply (rule subst_eqtyparg)
 apply (rule comp_rls)
-apply (tactic {* typechk_tac @{thms assms} *})
+apply (tactic {* typechk_tac @{context} @{thms assms} *})
 apply assumption
 done
 
@@ -183,11 +183,11 @@
 apply (tactic {* biresolve_tac safe_brls 2 *})
 (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
 apply (rule_tac [2] a = "y" in ProdE)
-apply (tactic {* typechk_tac @{thms assms} *})
+apply (tactic {* typechk_tac @{context} @{thms assms} *})
 apply (rule SumE, assumption)
-apply (tactic "intr_tac []")
-apply (tactic "TRYALL assume_tac")
-apply (tactic {* typechk_tac @{thms assms} *})
+apply (tactic "intr_tac @{context} []")
+apply (tactic "TRYALL (assume_tac @{context})")
+apply (tactic {* typechk_tac @{context} @{thms assms} *})
 done
 
 end
--- a/src/CTT/ex/Equality.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CTT/ex/Equality.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -12,27 +12,27 @@
 lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
 apply (rule EqE)
 apply (rule elim_rls, assumption)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 lemma when_eq: "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B"
 apply (rule EqE)
 apply (rule elim_rls, assumption)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 (*in the "rec" formulation of addition, 0+n=n *)
 lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N"
 apply (rule EqE)
 apply (rule elim_rls, assumption)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 (*the harder version, n+0=n: recursive, uses induction hypothesis*)
 lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N"
 apply (rule EqE)
 apply (rule elim_rls, assumption)
-apply (tactic "hyp_rew_tac []")
+apply (tactic "hyp_rew_tac @{context} []")
 done
 
 (*Associativity of addition*)
@@ -40,19 +40,19 @@
       ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) =
           rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N"
 apply (tactic {* NE_tac @{context} "a" 1 *})
-apply (tactic "hyp_rew_tac []")
+apply (tactic "hyp_rew_tac @{context} []")
 done
 
 (*Martin-Lof (1984) page 62: pairing is surjective*)
 lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)"
 apply (rule EqE)
 apply (rule elim_rls, assumption)
-apply (tactic {* DEPTH_SOLVE_1 (rew_tac []) *}) (*!!!!!!!*)
+apply (tactic {* DEPTH_SOLVE_1 (rew_tac @{context} []) *}) (*!!!!!!!*)
 done
 
 lemma "[| a : A;  b : B |] ==>
      (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 (*a contrived, complicated simplication, requires sum-elimination also*)
@@ -61,9 +61,9 @@
 apply (rule reduction_rls)
 apply (rule_tac [3] intrL_rls)
 apply (rule_tac [4] EqE)
-apply (rule_tac [4] SumE, tactic "assume_tac 4")
+apply (rule_tac [4] SumE, tactic "assume_tac @{context} 4")
 (*order of unifiers is essential here*)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 end
--- a/src/CTT/ex/Synthesis.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CTT/ex/Synthesis.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -12,21 +12,21 @@
 text "discovery of predecessor function"
 schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
                   *  (PROD n:N. Eq(N, pred ` succ(n), n))"
-apply (tactic "intr_tac []")
-apply (tactic eqintr_tac)
+apply (tactic "intr_tac @{context} []")
+apply (tactic "eqintr_tac @{context}")
 apply (rule_tac [3] reduction_rls)
 apply (rule_tac [5] comp_rls)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 text "the function fst as an element of a function type"
 schematic_lemma [folded basic_defs]:
   "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
-apply (tactic "intr_tac []")
-apply (tactic eqintr_tac)
+apply (tactic "intr_tac @{context} []")
+apply (tactic "eqintr_tac @{context}")
 apply (rule_tac [2] reduction_rls)
 apply (rule_tac [4] comp_rls)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 txt "now put in A everywhere"
 apply assumption+
 done
@@ -36,10 +36,10 @@
   See following example.*)
 schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
                    * Eq(?A, ?b(inr(i)), <succ(0), i>)"
-apply (tactic "intr_tac []")
-apply (tactic eqintr_tac)
+apply (tactic "intr_tac @{context} []")
+apply (tactic "eqintr_tac @{context}")
 apply (rule comp_rls)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 (*Here we allow the type to depend on i.
@@ -55,13 +55,13 @@
 schematic_lemma [folded basic_defs]:
   "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
                            *  Eq(?A, ?b(inr(<i,j>)), j)"
-apply (tactic "intr_tac []")
-apply (tactic eqintr_tac)
+apply (tactic "intr_tac @{context} []")
+apply (tactic "eqintr_tac @{context}")
 apply (rule PlusC_inl [THEN trans_elem])
 apply (rule_tac [4] comp_rls)
 apply (rule_tac [7] reduction_rls)
 apply (rule_tac [10] comp_rls)
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 (*similar but allows the type to depend on i and j*)
@@ -79,10 +79,10 @@
 schematic_lemma [folded arith_defs]:
   "?c : PROD n:N. Eq(N, ?f(0,n), n)
                   *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
-apply (tactic "intr_tac []")
-apply (tactic eqintr_tac)
+apply (tactic "intr_tac @{context} []")
+apply (tactic "eqintr_tac @{context}")
 apply (rule comp_rls)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 text "The addition function -- using explicit lambdas"
@@ -90,15 +90,15 @@
   "?c : SUM plus : ?A .
          PROD x:N. Eq(N, plus`0`x, x)
                 *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
-apply (tactic "intr_tac []")
-apply (tactic eqintr_tac)
+apply (tactic "intr_tac @{context} []")
+apply (tactic "eqintr_tac @{context}")
 apply (tactic "resolve_tac [TSimp.split_eqn] 3")
-apply (tactic "SELECT_GOAL (rew_tac []) 4")
+apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
 apply (tactic "resolve_tac [TSimp.split_eqn] 3")
-apply (tactic "SELECT_GOAL (rew_tac []) 4")
+apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
 apply (rule_tac [3] p = "y" in NC_succ)
   (**  by (resolve_tac comp_rls 3);  caused excessive branching  **)
-apply (tactic "rew_tac []")
+apply (tactic "rew_tac @{context} []")
 done
 
 end
--- a/src/CTT/ex/Typechecking.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CTT/ex/Typechecking.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -34,34 +34,34 @@
 subsection {* Multi-step proofs: Type inference *}
 
 lemma "PROD w:N. N + N type"
-apply (tactic form_tac)
+apply (tactic "form_tac @{context}")
 done
 
 schematic_lemma "<0, succ(0)> : ?A"
-apply (tactic "intr_tac []")
+apply (tactic "intr_tac @{context} []")
 done
 
 schematic_lemma "PROD w:N . Eq(?A,w,w) type"
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 text "typechecking an application of fst"
 schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 text "typechecking the predecessor function"
 schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 text "typechecking the addition function"
 schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 done
 
 (*Proofs involving arbitrary types.
@@ -69,18 +69,18 @@
 ML {* val N_tac = TRYALL (rtac @{thm NF}) *}
 
 schematic_lemma "lam w. <w,w> : ?A"
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 apply (tactic N_tac)
 done
 
 schematic_lemma "lam x. lam y. x : ?A"
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 apply (tactic N_tac)
 done
 
 text "typechecking fst (as a function object)"
 schematic_lemma "lam i. split(i, %j k. j) : ?A"
-apply (tactic "typechk_tac []")
+apply (tactic "typechk_tac @{context} []")
 apply (tactic N_tac)
 done
 
--- a/src/CTT/rew.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/CTT/rew.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -23,7 +23,7 @@
   val trans_red         = @{thm trans_red}
   val red_if_equal      = @{thm red_if_equal}
   val default_rls       = @{thms comp_rls}
-  val routine_tac       = routine_tac (@{thms routine_rls})
+  val routine_tac       = routine_tac @{thms routine_rls}
   end;
 
 structure TSimp = TSimpFun (TSimp_data);
@@ -31,12 +31,12 @@
 val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls};
 
 (*Make a rewriting tactic from a normalization tactic*)
-fun make_rew_tac ntac =
-    TRY eqintr_tac  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  
+fun make_rew_tac ctxt ntac =
+    TRY (eqintr_tac ctxt)  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  
     ntac;
 
-fun rew_tac thms = make_rew_tac
-    (TSimp.norm_tac(standard_congr_rls, thms));
+fun rew_tac ctxt thms = make_rew_tac ctxt
+    (TSimp.norm_tac ctxt (standard_congr_rls, thms));
 
-fun hyp_rew_tac thms = make_rew_tac
-    (TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms));
+fun hyp_rew_tac ctxt thms = make_rew_tac ctxt
+    (TSimp.cond_norm_tac ctxt (prove_cond_tac, standard_congr_rls, thms));
--- a/src/Doc/Implementation/Tactic.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Doc/Implementation/Tactic.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -282,7 +282,7 @@
   @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
   @{index_ML forward_tac: "thm list -> int -> tactic"} \\
   @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
-  @{index_ML assume_tac: "int -> tactic"} \\
+  @{index_ML assume_tac: "Proof.context -> int -> tactic"} \\
   @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
   @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
   @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
@@ -324,7 +324,7 @@
   elimination rules, which is useful to organize the search process
   systematically in proof tools.
 
-  \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
+  \item @{ML assume_tac}~@{text "ctxt i"} attempts to solve subgoal @{text i}
   by assumption (modulo higher-order unification).
 
   \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
--- a/src/Doc/Isar_Ref/Generic.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -1053,7 +1053,7 @@
 
 ML \<open>
   fun subgoaler_tac ctxt =
-    assume_tac ORELSE'
+    assume_tac ctxt ORELSE'
     resolve_tac (Simplifier.prems_of ctxt) ORELSE'
     asm_simp_tac ctxt
 \<close>
--- a/src/Doc/Tutorial/Protocol/Event.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -260,10 +260,10 @@
 
 ML
 {*
-val analz_mono_contra_tac = 
+fun analz_mono_contra_tac ctxt =
   rtac @{thm analz_impI} THEN' 
   REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
-  THEN' mp_tac
+  THEN' mp_tac ctxt
 *}
 
 lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
@@ -285,7 +285,7 @@
     intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
 
 method_setup analz_mono_contra = {*
-    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
@@ -330,7 +330,7 @@
 val knows_Spy_subset_knows_Spy_Gets = @{thm knows_Spy_subset_knows_Spy_Gets};
 
 
-val synth_analz_mono_contra_tac = 
+fun synth_analz_mono_contra_tac ctxt = 
   rtac @{thm syan_impI} THEN'
   REPEAT1 o 
     (dresolve_tac 
@@ -338,11 +338,11 @@
       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
   THEN'
-  mp_tac
+  mp_tac ctxt
 *}
 
 method_setup synth_analz_mono_contra = {*
-    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *}
     "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
 (*>*)
 
--- a/src/FOL/IFOL.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOL/IFOL.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -208,7 +208,7 @@
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
 ML {*
-  fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  assume_tac i
+  fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  atac i
   fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  eq_assume_tac i
 *}
 
--- a/src/FOL/intprover.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOL/intprover.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -20,7 +20,7 @@
   val best_tac: Proof.context -> int -> tactic
   val best_dup_tac: Proof.context -> int -> tactic
   val fast_tac: Proof.context -> int -> tactic
-  val inst_step_tac: int -> tactic
+  val inst_step_tac: Proof.context -> int -> tactic
   val safe_step_tac: Proof.context -> int -> tactic
   val safe_brls: (bool * thm) list
   val safe_tac: Proof.context -> tactic
@@ -74,14 +74,14 @@
 fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
 
 (*These steps could instantiate variables and are therefore unsafe.*)
-val inst_step_tac =
-  assume_tac APPEND' mp_tac APPEND' 
+fun inst_step_tac ctxt =
+  assume_tac ctxt APPEND' mp_tac APPEND' 
   biresolve_tac (safe0_brls @ safep_brls);
 
 (*One safe or unsafe step. *)
-fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i];
+fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_brls i];
 
-fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i];
+fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_dup_brls i];
 
 (*Dumb but fast*)
 fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
--- a/src/FOL/simpdata.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOL/simpdata.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -108,7 +108,7 @@
 
 fun unsafe_solver ctxt =
   FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt),
-    assume_tac,
+    assume_tac ctxt,
     eresolve_tac @{thms FalseE}];
 
 (*No premature instantiation of variables during simplification*)
--- a/src/FOLP/IFOLP.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOLP/IFOLP.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -252,7 +252,7 @@
 local
   fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P;
 in
-val uniq_assume_tac =
+fun uniq_assume_tac ctxt =
   SUBGOAL
     (fn (prem,i) =>
       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
@@ -260,7 +260,7 @@
       in
           if exists (fn hyp => hyp aconv concl) hyps
           then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
-                   [_] => assume_tac i
+                   [_] => assume_tac ctxt i
                  |  _  => no_tac
           else no_tac
       end);
@@ -272,12 +272,14 @@
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
 ML {*
-  fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac i
+  fun mp_tac ctxt i =
+    eresolve_tac [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac ctxt i
 *}
 
 (*Like mp_tac but instantiates no variables*)
 ML {*
-  fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  uniq_assume_tac i
+  fun int_uniq_mp_tac ctxt i =
+    eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  uniq_assume_tac ctxt i
 *}
 
 
@@ -374,7 +376,7 @@
 
 schematic_lemma disj_cong:
   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
-  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
+  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
   done
 
 schematic_lemma imp_cong:
@@ -382,31 +384,31 @@
     and "!!x. x:P' ==> q(x):Q <-> Q'"
   shows "?p:(P-->Q) <-> (P'-->Q')"
   apply (insert assms(1))
-  apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} |
+  apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac @{context} 1 *} |
     tactic {* iff_tac @{thms assms} 1 *})+
   done
 
 schematic_lemma iff_cong:
   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
-  apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
+  apply (erule iffE | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
   done
 
 schematic_lemma not_cong:
   "p:P <-> P' ==> ?p:~P <-> ~P'"
-  apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
+  apply (assumption | rule iffI notI | tactic {* mp_tac @{context} 1 *} | erule iffE notE)+
   done
 
 schematic_lemma all_cong:
   assumes "!!x. f(x):P(x) <-> Q(x)"
   shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
-  apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
+  apply (assumption | rule iffI allI | tactic {* mp_tac @{context} 1 *} | erule allE |
     tactic {* iff_tac @{thms assms} 1 *})+
   done
 
 schematic_lemma ex_cong:
   assumes "!!x. f(x):P(x) <-> Q(x)"
   shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
-  apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
+  apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac @{context} 1 *} |
     tactic {* iff_tac @{thms assms} 1 *})+
   done
 
@@ -636,7 +638,7 @@
   "?p6 : P & ~P <-> False"
   "?p7 : ~P & P <-> False"
   "?p8 : (P & Q) & R <-> P & (Q & R)"
-  apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
+  apply (tactic {* fn st => IntPr.fast_tac @{context} 1 st *})+
   done
 
 schematic_lemma disj_rews:
@@ -646,13 +648,13 @@
   "?p4 : False | P <-> P"
   "?p5 : P | P <-> P"
   "?p6 : (P | Q) | R <-> P | (Q | R)"
-  apply (tactic {* IntPr.fast_tac 1 *})+
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
   done
 
 schematic_lemma not_rews:
   "?p1 : ~ False <-> True"
   "?p2 : ~ True <-> False"
-  apply (tactic {* IntPr.fast_tac 1 *})+
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
   done
 
 schematic_lemma imp_rews:
@@ -662,7 +664,7 @@
   "?p4 : (True --> P) <-> P"
   "?p5 : (P --> P) <-> True"
   "?p6 : (P --> ~P) <-> ~P"
-  apply (tactic {* IntPr.fast_tac 1 *})+
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
   done
 
 schematic_lemma iff_rews:
@@ -671,13 +673,13 @@
   "?p3 : (P <-> P) <-> True"
   "?p4 : (False <-> P) <-> ~P"
   "?p5 : (P <-> False) <-> ~P"
-  apply (tactic {* IntPr.fast_tac 1 *})+
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
   done
 
 schematic_lemma quant_rews:
   "?p1 : (ALL x. P) <-> P"
   "?p2 : (EX x. P) <-> P"
-  apply (tactic {* IntPr.fast_tac 1 *})+
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
   done
 
 (*These are NOT supplied by default!*)
@@ -686,7 +688,7 @@
   "?p2 : P & (Q | R) <-> P&Q | P&R"
   "?p3 : (Q | R) & P <-> Q&P | R&P"
   "?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)"
-  apply (tactic {* IntPr.fast_tac 1 *})+
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
   done
 
 schematic_lemma distrib_rews2:
@@ -694,17 +696,17 @@
   "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
   "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
   "?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"
-  apply (tactic {* IntPr.fast_tac 1 *})+
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
   done
 
 lemmas distrib_rews = distrib_rews1 distrib_rews2
 
 schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
-  apply (tactic {* IntPr.fast_tac 1 *})
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})
   done
 
 schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
-  apply (tactic {* IntPr.fast_tac 1 *})
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})
   done
 
 end
--- a/src/FOLP/classical.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOLP/classical.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -45,17 +45,17 @@
        safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
        haz_brls: (bool*thm)list}
   val best_tac : Proof.context -> claset -> int -> tactic
-  val contr_tac : int -> tactic
+  val contr_tac : Proof.context -> int -> tactic
   val fast_tac : Proof.context -> claset -> int -> tactic
-  val inst_step_tac : int -> tactic
+  val inst_step_tac : Proof.context -> int -> tactic
   val joinrules : thm list * thm list -> (bool * thm) list
-  val mp_tac: int -> tactic
+  val mp_tac: Proof.context -> int -> tactic
   val safe_tac : Proof.context -> claset -> tactic
   val safe_step_tac : Proof.context -> claset -> int -> tactic
   val slow_step_tac : Proof.context -> claset -> int -> tactic
   val step_tac : Proof.context -> claset -> int -> tactic
   val swapify : thm list -> thm list
-  val swap_res_tac : thm list -> int -> tactic
+  val swap_res_tac : Proof.context -> thm list -> int -> tactic
   val uniq_mp_tac: Proof.context -> int -> tactic
   end;
 
@@ -70,22 +70,22 @@
 val imp_elim = make_elim mp;
 
 (*Solve goal that assumes both P and ~P. *)
-val contr_tac = etac not_elim THEN'  assume_tac;
+fun contr_tac ctxt = etac not_elim THEN'  assume_tac ctxt;
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
-fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
+fun mp_tac ctxt i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac ctxt i;
 
 (*Like mp_tac but instantiates no variables*)
-fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
+fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac ctxt i;
 
 (*Creates rules to eliminate ~A, from rules to introduce A*)
 fun swapify intrs = intrs RLN (2, [swap]);
 
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
-fun swap_res_tac rls = 
+fun swap_res_tac ctxt rls = 
     let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))
-    in  assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)
+    in  assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls)
     end;
 
 
@@ -149,7 +149,7 @@
 
 (*Attack subgoals using safe inferences*)
 fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 
-  FIRST' [uniq_assume_tac,
+  FIRST' [uniq_assume_tac ctxt,
           uniq_mp_tac ctxt,
           biresolve_tac safe0_brls,
           FIRST' hyp_subst_tacs,
@@ -159,12 +159,12 @@
 fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
 
 (*These steps could instantiate variables and are therefore unsafe.*)
-val inst_step_tac = assume_tac APPEND' contr_tac;
+fun inst_step_tac ctxt = assume_tac ctxt APPEND' contr_tac ctxt;
 
 (*Single step for the prover.  FAILS unless it makes progress. *)
 fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 
   FIRST [safe_tac ctxt cs,
-         inst_step_tac i,
+         inst_step_tac ctxt i,
          biresolve_tac haz_brls i];
 
 (*** The following tactics all fail unless they solve one goal ***)
@@ -179,7 +179,7 @@
 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   allows backtracking from "safe" rules to "unsafe" rules here.*)
 fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 
-    safe_tac ctxt cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
+    safe_tac ctxt cs ORELSE (assume_tac ctxt i APPEND biresolve_tac haz_brls i);
 
 end; 
 end;
--- a/src/FOLP/ex/Intuitionistic.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOLP/ex/Intuitionistic.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -31,39 +31,39 @@
 begin
 
 schematic_lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ~~~P <-> ~P"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 subsection {* Lemmas for the propositional double-negation translation *}
 
 schematic_lemma "?p : P --> ~~P"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ~~(~~P --> P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 subsection {* The following are classically but not constructively valid *}
 
 (*The attempt to prove them terminates quickly!*)
 schematic_lemma "?p : ((P-->Q) --> P)  -->  P"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 schematic_lemma "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 
@@ -71,74 +71,74 @@
 
 text "Problem ~~1"
 schematic_lemma "?p : ~~((P-->Q)  <->  (~Q --> ~P))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~2"
 schematic_lemma "?p : ~~(~~P  <->  P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem 3"
 schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~4"
 schematic_lemma "?p : ~~((~P-->Q)  <->  (~Q --> P))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~5"
 schematic_lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~6"
 schematic_lemma "?p : ~~(P | ~P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~7"
 schematic_lemma "?p : ~~(P | ~~~P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~8.  Peirce's law"
 schematic_lemma "?p : ~~(((P-->Q) --> P)  -->  P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem 9"
 schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem 10"
 schematic_lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "11.  Proved in each direction (incorrectly, says Pelletier!!) "
 schematic_lemma "?p : P<->P"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~12.  Dijkstra's law  "
 schematic_lemma "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem 13.  Distributive law"
 schematic_lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~14"
 schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~15"
 schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~16"
 schematic_lemma "?p : ~~((P-->Q) | (Q-->P))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~17"
 schematic_lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
-  by (tactic {* IntPr.fast_tac 1 *})  -- slow
+  by (tactic {* IntPr.fast_tac @{context} 1 *})  -- slow
 
 
 subsection {* Examples with quantifiers *}
@@ -146,43 +146,43 @@
 text "The converse is classical in the following implications..."
 
 schematic_lemma "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "The following are not constructively valid!"
 text "The attempt to prove them terminates quickly!"
 
 schematic_lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 schematic_lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 schematic_lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 schematic_lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
 schematic_lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 
@@ -204,7 +204,7 @@
 text "Problem 20"
 schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
     --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem 21"
 schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
@@ -212,21 +212,21 @@
 
 text "Problem 22"
 schematic_lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem ~~23"
 schematic_lemma "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 text "Problem 24"
 schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
      (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
     --> ~~(EX x. P(x)&R(x))"
 (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
-  apply (tactic "IntPr.safe_tac")
+  apply (tactic "IntPr.safe_tac @{context}")
   apply (erule impE)
-   apply (tactic "IntPr.fast_tac 1")
-  apply (tactic "IntPr.fast_tac 1")
+   apply (tactic "IntPr.fast_tac @{context} 1")
+  apply (tactic "IntPr.fast_tac @{context} 1")
   done
 
 text "Problem 25"
@@ -235,72 +235,72 @@
         (ALL x. P(x) --> (M(x) & L(x))) &    
         ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))   
     --> (EX x. Q(x)&P(x))"
-  by (tactic "IntPr.best_tac 1")
+  by (tactic "IntPr.best_tac @{context} 1")
 
 text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
 schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
     --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
          (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 text "Problem ~~30"
 schematic_lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &  
         (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
     --> (ALL x. ~~S(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 text "Problem 31"
 schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
         (EX x. L(x) & P(x)) &  
         (ALL x. ~ R(x) --> M(x))   
     --> (EX x. L(x) & M(x))"
-  by (tactic "IntPr.fast_tac 1")
+  by (tactic "IntPr.fast_tac @{context} 1")
 
 text "Problem 32"
 schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
         (ALL x. S(x) & R(x) --> L(x)) &  
         (ALL x. M(x) --> R(x))   
     --> (ALL x. P(x) & M(x) --> L(x))"
-  by (tactic "IntPr.best_tac 1") -- slow
+  by (tactic "IntPr.best_tac @{context} 1") -- slow
 
 text "Problem 39"
 schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
-  by (tactic "IntPr.best_tac 1")
+  by (tactic "IntPr.best_tac @{context} 1")
 
 text "Problem 40.  AMENDED"
 schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
               ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
-  by (tactic "IntPr.best_tac 1") -- slow
+  by (tactic "IntPr.best_tac @{context} 1") -- slow
 
 text "Problem 44"
 schematic_lemma "?p : (ALL x. f(x) -->                                    
               (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
               (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
               --> (EX x. j(x) & ~f(x))"
-  by (tactic "IntPr.best_tac 1")
+  by (tactic "IntPr.best_tac @{context} 1")
 
 text "Problem 48"
 schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-  by (tactic "IntPr.best_tac 1")
+  by (tactic "IntPr.best_tac @{context} 1")
 
 text "Problem 51"
 schematic_lemma
     "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
      (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
-  by (tactic "IntPr.best_tac 1") -- {*60 seconds*}
+  by (tactic "IntPr.best_tac @{context} 1") -- {*60 seconds*}
 
 text "Problem 56"
 schematic_lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
-  by (tactic "IntPr.best_tac 1")
+  by (tactic "IntPr.best_tac @{context} 1")
 
 text "Problem 57"
 schematic_lemma
     "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
      (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
-  by (tactic "IntPr.best_tac 1")
+  by (tactic "IntPr.best_tac @{context} 1")
 
 text "Problem 60"
 schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
-  by (tactic "IntPr.best_tac 1")
+  by (tactic "IntPr.best_tac @{context} 1")
 
 end
--- a/src/FOLP/ex/Propositional_Int.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOLP/ex/Propositional_Int.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -12,106 +12,106 @@
 
 text "commutative laws of & and | "
 schematic_lemma "?p : P & Q  -->  Q & P"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : P | Q  -->  Q | P"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "associative laws of & and | "
 schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "distributive laws of & and | "
 schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "Laws involving implication"
 
 schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "Propositions-as-types"
 
 (*The combinator K*)
 schematic_lemma "?p : P --> (Q --> P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 (*The combinator S*)
 schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 (*Converse is classical*)
 schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "Schwichtenberg's examples (via T. Nipkow)"
 
 schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
               --> ((P --> Q) --> P) --> P"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
                --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
   
 schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
           --> (((P8 --> P2) --> P9) --> P3 --> P10)  
           --> (P1 --> P8) --> P6 --> P7  
           --> (((P3 --> P2) --> P9) --> P4)  
           --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
      --> (((P3 --> P2) --> P9) --> P4)  
      --> (((P6 --> P1) --> P2) --> P9)  
      --> (((P7 --> P1) --> P10) --> P4 --> P5)  
      --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 end
--- a/src/FOLP/ex/Quantifiers_Int.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOLP/ex/Quantifiers_Int.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -11,91 +11,91 @@
 begin
 
 schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 (*Converse is false*)
 schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "Some harder ones"
 
 schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 (*Converse is false*)
 schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "Basic test of quantifier reasoning"
 (*TRUE*)
 schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "The following should fail, as they are false!"
 
 schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
-  apply (tactic {* IntPr.fast_tac 1 *})?
+  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   oops
 
 
 text "Back to things that are provable..."
 
 schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 (*An example of why exI should be delayed as long as possible*)
 schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 
 text "Some slow ones"
 
 (*Principia Mathematica *11.53  *)
 schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 (*Principia Mathematica *11.55  *)
 schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 (*Principia Mathematica *11.61  *)
 schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
-  by (tactic {* IntPr.fast_tac 1 *})
+  by (tactic {* IntPr.fast_tac @{context} 1 *})
 
 end
--- a/src/FOLP/intprover.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOLP/intprover.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -15,13 +15,13 @@
 
 signature INT_PROVER = 
   sig
-  val best_tac: int -> tactic
-  val fast_tac: int -> tactic
-  val inst_step_tac: int -> tactic
-  val safe_step_tac: int -> tactic
+  val best_tac: Proof.context -> int -> tactic
+  val fast_tac: Proof.context -> int -> tactic
+  val inst_step_tac: Proof.context -> int -> tactic
+  val safe_step_tac: Proof.context -> int -> tactic
   val safe_brls: (bool * thm) list
-  val safe_tac: tactic
-  val step_tac: int -> tactic
+  val safe_tac: Proof.context -> tactic
+  val step_tac: Proof.context -> int -> tactic
   val haz_brls: (bool * thm) list
   end;
 
@@ -52,26 +52,26 @@
     List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
 
 (*Attack subgoals using safe inferences*)
-val safe_step_tac = FIRST' [uniq_assume_tac,
-                            int_uniq_mp_tac,
+fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt,
+                            int_uniq_mp_tac ctxt,
                             biresolve_tac safe0_brls,
                             hyp_subst_tac,
                             biresolve_tac safep_brls] ;
 
 (*Repeatedly attack subgoals using safe inferences*)
-val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
+fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt));
 
 (*These steps could instantiate variables and are therefore unsafe.*)
-val inst_step_tac = assume_tac APPEND' mp_tac;
+fun inst_step_tac ctxt = assume_tac ctxt APPEND' mp_tac ctxt;
 
 (*One safe or unsafe step. *)
-fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
+fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_brls i];
 
 (*Dumb but fast*)
-val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
+fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
 
 (*Slower but smarter than fast_tac*)
-val best_tac = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
+fun best_tac ctxt =
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
 
 end;
--- a/src/FOLP/simp.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOLP/simp.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -451,7 +451,7 @@
                      thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
             end
     | NONE => if more
-            then rew((lhs_net_tac anet i THEN assume_tac i) thm,
+            then rew((lhs_net_tac anet i THEN atac i) thm,
                      thm,ss,anet,ats,cs,false)
             else (ss,thm,anet,ats,cs);
 
--- a/src/HOL/Auth/Event.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Auth/Event.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -270,14 +270,14 @@
 
 ML
 {*
-val analz_mono_contra_tac = 
+fun analz_mono_contra_tac ctxt = 
   rtac @{thm analz_impI} THEN' 
   REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
-  THEN' mp_tac
+  THEN' (mp_tac ctxt)
 *}
 
 method_setup analz_mono_contra = {*
-    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
@@ -286,7 +286,7 @@
 
 ML
 {*
-val synth_analz_mono_contra_tac = 
+fun synth_analz_mono_contra_tac ctxt = 
   rtac @{thm syan_impI} THEN'
   REPEAT1 o 
     (dresolve_tac 
@@ -294,11 +294,11 @@
       @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
       @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
   THEN'
-  mp_tac
+  mp_tac ctxt
 *}
 
 method_setup synth_analz_mono_contra = {*
-    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *}
     "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
 
 end
--- a/src/HOL/Auth/Recur.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Auth/Recur.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -163,7 +163,7 @@
                                   [THEN respond.Cons, THEN respond.Cons]],
                      THEN recur.RA4, THEN recur.RA4])
 apply basic_possibility
-apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
+apply (tactic "DEPTH_SOLVE (swap_res_tac @{context} [refl, conjI, disjCI] 1)")
 done
 
 
--- a/src/HOL/Bali/AxSem.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Bali/AxSem.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -661,13 +661,14 @@
 lemma ax_thin [rule_format (no_asm)]: 
   "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
 apply (erule ax_derivs.induct)
-apply                (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
+apply                (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1])")
 apply                (rule ax_derivs.empty)
 apply               (erule (1) ax_derivs.insert)
 apply              (fast intro: ax_derivs.asm)
 (*apply           (fast intro: ax_derivs.cut) *)
 apply            (fast intro: ax_derivs.weaken)
-apply           (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) 
+apply           (rule ax_derivs.conseq, intro strip, tactic "smp_tac @{context} 3 1",clarify,
+  tactic "smp_tac @{context} 1 1",rule exI, rule exI, erule (1) conjI) 
 (* 37 subgoals *)
 prefer 18 (* Methd *)
 apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
@@ -700,7 +701,7 @@
 apply     (fast intro: ax_derivs.asm)
 (*apply  (blast intro: ax_derivs.cut) *)
 apply   (fast intro: ax_derivs.weaken)
-apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
+apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac @{context} 3 1", blast(* unused *))
 (*37 subgoals*)
 apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros}) 
                    THEN_ALL_NEW fast_tac @{context}) *})
--- a/src/HOL/Bali/AxSound.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Bali/AxSound.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -50,13 +50,13 @@
 apply (rule iffI)
 apply  fast
 apply clarify
-apply (tactic "smp_tac 3 1")
+apply (tactic "smp_tac @{context} 3 1")
 apply (case_tac "normal s")
 apply  clarsimp
 apply  (elim conjE impE)
 apply    blast
 
-apply    (tactic "smp_tac 2 1")
+apply    (tactic "smp_tac @{context} 2 1")
 apply    (drule evaln_eval)
 apply    (drule (1) eval_type_sound [THEN conjunct1],simp, assumption+)
 apply    simp
@@ -84,7 +84,7 @@
 "\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk> 
   \<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
 apply (simp (no_asm_use) add: triple_valid2_def2)
-apply (intro strip, tactic "smp_tac 3 1", clarify)
+apply (intro strip, tactic "smp_tac @{context} 3 1", clarify)
 apply (erule wt_elim_cases, erule da_elim_cases, erule evaln_elim_cases)
 apply (unfold body_def Let_def)
 apply (clarsimp simp add: inj_term_simps)
@@ -400,14 +400,14 @@
       from valid_A conf wt da eval P con
       have "Q v s1 Z"
         apply (simp add: ax_valids2_def triple_valid2_def2)
-        apply (tactic "smp_tac 3 1")
+        apply (tactic "smp_tac @{context} 3 1")
         apply clarify
-        apply (tactic "smp_tac 1 1")
+        apply (tactic "smp_tac @{context} 1 1")
         apply (erule allE,erule allE, erule mp)
         apply (intro strip)
-        apply (tactic "smp_tac 3 1")
-        apply (tactic "smp_tac 2 1")
-        apply (tactic "smp_tac 1 1")
+        apply (tactic "smp_tac @{context} 3 1")
+        apply (tactic "smp_tac @{context} 2 1")
+        apply (tactic "smp_tac @{context} 1 1")
         by blast
       moreover have "s1\<Colon>\<preceq>(G, L)"
       proof (cases "normal s0")
@@ -2065,7 +2065,7 @@
                           (abupd (absorb (Cont l')) s2') \<diamondsuit> s3'"
                   apply (simp only: True if_True eqs)
                   apply (elim conjE)
-                  apply (tactic "smp_tac 3 1")
+                  apply (tactic "smp_tac @{context} 3 1")
                   apply fast
                   done
                 from eval_e
--- a/src/HOL/Bali/Evaln.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Bali/Evaln.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -449,7 +449,7 @@
   "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
 apply (erule evaln.induct)
 apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
-  REPEAT o smp_tac 1, 
+  REPEAT o smp_tac @{context} 1, 
   resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
 (* 3 subgoals *)
 apply (auto split del: split_if)
--- a/src/HOL/Bali/Table.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Bali/Table.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -396,7 +396,7 @@
 apply (rename_tac "ba")
 apply (drule_tac x = "ba" in spec)
 apply clarify
-apply (tactic "smp_tac 2 1")
+apply (tactic "smp_tac @{context} 2 1")
 apply (erule (1) notE impE)
 apply (case_tac "aa = b")
 apply fast+
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -80,7 +80,7 @@
        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
        TRY (simp_tac simpset3 1), TRY (simp_tac (put_simpset cooper_ss ctxt) 1)]
       (Thm.trivial ct))
-    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
+    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
     (* The result of the quantifier elimination *)
     val (th, tac) =
       (case (prop_of pre_thm) of
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -61,7 +61,7 @@
       [simp_tac simpset0 1,
        TRY (simp_tac (put_simpset ferrack_ss ctxt) 1)]
       (Thm.trivial ct))
-    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
+    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case prop_of pre_thm of
         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -108,7 +108,7 @@
        TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
        TRY (simp_tac (put_simpset mir_ss ctxt) 1)]
       (Thm.trivial ct))
-    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
+    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
     (* The result of the quantifier elimination *)
     val (th, tac) = case (prop_of pre_thm) of
         Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
--- a/src/HOL/HOL.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/HOL.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -1982,7 +1982,7 @@
     val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
   in
     fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
-    fun smp_tac j = EVERY'[dresolve_tac (smp j), assume_tac];
+    fun smp_tac ctxt j = EVERY'[dresolve_tac (smp j), assume_tac ctxt];
   end;
 
   local
--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -199,7 +199,7 @@
 apply (drule spec, erule impE)
 apply  (erule BufAC_Asm_antiton [THEN antitonPD])
 apply  (erule is_ub_thelub)
-apply (tactic "smp_tac 3 1")
+apply (tactic "smp_tac @{context} 3 1")
 apply (drule is_ub_thelub)
 apply (drule (1) mp)
 apply (drule (1) mp)
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -777,7 +777,7 @@
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
 apply(tactic {* TRYALL (etac disjE) *})
 apply simp_all
-apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *})
 apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
 apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
 done
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -1187,7 +1187,7 @@
 --{* 72 subgoals left *}
 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
 --{* 35 subgoals left *}
-apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
+apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *})
 --{* 28 subgoals left *}
 apply(tactic {* TRYALL (etac conjE) *})
 apply(tactic {* TRYALL (etac disjE) *})
--- a/src/HOL/IMPP/Hoare.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/IMPP/Hoare.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -209,13 +209,13 @@
 *)
 lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
 apply (erule hoare_derivs.induct)
-apply                (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1]) *})
+apply                (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
 apply (rule hoare_derivs.empty)
 apply               (erule (1) hoare_derivs.insert)
 apply              (fast intro: hoare_derivs.asm)
 apply             (fast intro: hoare_derivs.cut)
 apply            (fast intro: hoare_derivs.weaken)
-apply           (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI)
+apply           (rule hoare_derivs.conseq, intro strip, tactic "smp_tac @{context} 2 1", clarify, tactic "smp_tac @{context} 1 1",rule exI, rule exI, erule (1) conjI)
 prefer 7
 apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
 apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *})
@@ -287,9 +287,9 @@
 apply        (blast) (* weaken *)
 apply       (tactic {* ALLGOALS (EVERY'
   [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
-   simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac 1]) *})
+   simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
 apply       (simp_all (no_asm_use) add: triple_valid_def2)
-apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
+apply       (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *)
 apply      (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *)
 prefer 3 apply   (force) (* Call *)
 apply  (erule_tac [2] evaln_elim_cases) (* If *)
--- a/src/HOL/IMPP/Misc.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/IMPP/Misc.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -71,12 +71,12 @@
 apply (simp (no_asm_use) add: triple_valid_def2)
 apply clarsimp
 apply (drule_tac x = "s<Y>" in spec)
-apply (tactic "smp_tac 1 1")
+apply (tactic "smp_tac @{context} 1 1")
 apply (drule spec)
 apply (drule_tac x = "s[Loc Y::=a s]" in spec)
 apply (simp (no_asm_use))
 apply (erule (1) notE impE)
-apply (tactic "smp_tac 1 1")
+apply (tactic "smp_tac @{context} 1 1")
 apply simp
 done
 
--- a/src/HOL/IMPP/Natural.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/IMPP/Natural.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -139,7 +139,8 @@
 lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
 apply (erule evalc.induct)
 apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
-apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac, REPEAT o eresolve_tac [exE, conjE]]) *})
+apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac @{context},
+  REPEAT o eresolve_tac [exE, conjE]]) *})
 apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
 done
 
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -138,7 +138,7 @@
 apply( drule (3) Call_lemma)
 apply( clarsimp simp add: wf_java_mdecl_def)
 apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
-apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac 2")
+apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
 apply(  rule conformsI)
 apply(   erule conforms_heapD)
 apply(  rule lconf_ext)
@@ -156,10 +156,10 @@
 apply(  fast intro: hext_trans)
 apply( rule conjI)
 apply(  rule_tac [2] impI)
-apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
+apply(  erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
 apply(  frule_tac [2] conf_widen)
-apply(    tactic "assume_tac 4")
-apply(   tactic "assume_tac 2")
+apply(    tactic "assume_tac @{context} 4")
+apply(   tactic "assume_tac @{context} 2")
 prefer 2
 apply(  fast elim!: widen_trans)
 apply (rule conforms_xcpt_change)
@@ -177,8 +177,9 @@
 declare wf_prog_ws_prog [simp]
 
 ML{*
-val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
-  (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
+fun forward_hyp_tac ctxt =
+  ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac ctxt,
+    (mp_tac ctxt ORELSE' (dtac spec THEN' mp_tac ctxt)), REPEAT o (etac conjE)]))
 *}
 
 
@@ -226,8 +227,8 @@
 apply( erule conf_litval)
 
 -- "13 BinOp"
-apply (tactic "forward_hyp_tac")
-apply (tactic "forward_hyp_tac")
+apply (tactic "forward_hyp_tac @{context}")
+apply (tactic "forward_hyp_tac @{context}")
 apply( rule conjI, erule (1) hext_trans)
 apply( erule conjI)
 apply( clarsimp)
@@ -246,7 +247,7 @@
 apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
   (asm_full_simp_tac @{context})) 7*})
 
-apply (tactic "forward_hyp_tac")
+apply (tactic "forward_hyp_tac @{context}")
 
 -- "11+1 if"
 prefer 7
@@ -294,7 +295,7 @@
 apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
 apply(force elim: hext_trans)
 
-apply (tactic "forward_hyp_tac")
+apply (tactic "forward_hyp_tac @{context}")
 
 -- "4 Cond"
 prefer 4
@@ -317,7 +318,7 @@
 apply( case_tac "x2")
   -- "x2 = None"
   apply (simp)
-  apply (tactic forward_hyp_tac, clarify)
+  apply (tactic "forward_hyp_tac @{context}", clarify)
   apply( drule eval_no_xcpt)
   apply( erule FAss_type_sound, rule HOL.refl, assumption+)
   -- "x2 = Some a"
--- a/src/HOL/NanoJava/AxSem.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -152,7 +152,7 @@
   "(A' |\<turnstile>  C         \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile>  C       )) \<and> 
    (A'  \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A  \<turnstile>\<^sub>e {P} e {Q}))"
 apply (rule hoare_ehoare.induct)
-apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
+apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1])")
 apply (blast intro: hoare_ehoare.Skip)
 apply (blast intro: hoare_ehoare.Comp)
 apply (blast intro: hoare_ehoare.Cond)
@@ -164,7 +164,7 @@
 apply (blast intro: hoare_ehoare.NewC)
 apply (blast intro: hoare_ehoare.Cast)
 apply (erule hoare_ehoare.Call)
-apply   (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption)
+apply   (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption)
 apply  blast
 apply (blast intro!: hoare_ehoare.Meth)
 apply (blast intro!: hoare_ehoare.Impl)
@@ -172,9 +172,9 @@
 apply (blast intro: hoare_ehoare.ConjI)
 apply (blast intro: hoare_ehoare.ConjE)
 apply (rule hoare_ehoare.Conseq)
-apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
+apply  (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption+)
 apply (rule hoare_ehoare.eConseq)
-apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
+apply  (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption+)
 done
 
 lemma cThin: "\<lbrakk>A' |\<turnstile> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
--- a/src/HOL/NanoJava/Equivalence.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -111,7 +111,7 @@
                  apply fast
                 apply fast
                apply fast
-              apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
+              apply (clarify,tactic "smp_tac @{context} 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
              apply fast
             apply fast
            apply fast
--- a/src/HOL/NanoJava/Example.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/NanoJava/Example.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -131,7 +131,7 @@
 apply  auto
 apply  (case_tac "aa=a")
 apply   auto
-apply (tactic "smp_tac 1 1")
+apply (tactic "smp_tac @{context} 1 1")
 apply (case_tac "aa=a")
 apply  auto
 done
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -438,11 +438,11 @@
         in
           fold (fn (s, tvs) => fn thy => Axclass.prove_arity
               (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
-              (fn _ => EVERY
+              (fn ctxt => EVERY
                 [Class.intro_classes_tac [],
                  resolve_tac perm_empty_thms 1,
                  resolve_tac perm_append_thms 1,
-                 resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
+                 resolve_tac perm_eq_thms 1, assume_tac ctxt 1]) thy)
             (full_new_type_names' ~~ tyvars) thy
         end) atoms |>
       Global_Theory.add_thmss
@@ -562,7 +562,7 @@
            [Old_Datatype_Aux.ind_tac rep_induct [] 1,
             ALLGOALS (simp_tac (ctxt addsimps
               (Thm.symmetric perm_fun_def :: abs_perm))),
-            ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
+            ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac ctxt)])),
         length new_type_names));
 
     val perm_closed_thmss = map mk_perm_closed atoms;
@@ -1721,9 +1721,9 @@
                       (S $ Free x $ Free y, P $ (Free y)))
                         (rec_unique_frees'' ~~ rec_unique_frees' ~~
                            rec_sets ~~ rec_preds)))))
-               (fn _ =>
+               (fn {context = ctxt, ...} =>
                   rtac rec_induct 1 THEN
-                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
+                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac ctxt) 1))));
            val rec_fin_supp_thms' = map
              (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
              (rec_fin_supp_thms ~~ finite_thss);
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -539,7 +539,7 @@
   Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
     (fn i =>
       EVERY [ftac @{thm Gets_certificate_valid} i,
-             assume_tac i,
+             assume_tac ctxt i,
              etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
 *}
 
--- a/src/HOL/SET_Protocol/Event_SET.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -182,14 +182,14 @@
 
 ML
 {*
-val analz_mono_contra_tac = 
+fun analz_mono_contra_tac ctxt = 
   rtac @{thm analz_impI} THEN' 
   REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
-  THEN' mp_tac
+  THEN' mp_tac ctxt
 *}
 
 method_setup analz_mono_contra = {*
-    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
+    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
     "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
 
 end
--- a/src/HOL/SET_Protocol/Purchase.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/SET_Protocol/Purchase.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -483,7 +483,7 @@
   Args.goal_spec >> (fn quant =>
     fn ctxt => SIMPLE_METHOD'' quant (fn i =>
       EVERY [ftac @{thm Gets_certificate_valid} i,
-             assume_tac i, REPEAT (hyp_subst_tac ctxt i)]))
+             assume_tac ctxt i, REPEAT (hyp_subst_tac ctxt i)]))
 *}
 
 
--- a/src/HOL/Set.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Set.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -383,7 +383,7 @@
 
 setup {*
   map_theory_claset (fn ctxt =>
-    ctxt addbefore ("bspec", fn _ => dresolve_tac @{thms bspec} THEN' assume_tac))
+    ctxt addbefore ("bspec", fn ctxt' => dresolve_tac @{thms bspec} THEN' assume_tac ctxt'))
 *}
 
 ML {*
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -227,7 +227,7 @@
   val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
   val fast_solver = mk_solver "fast_solver" (fn ctxt =>
     if Config.get ctxt config_fast_solver
-    then assume_tac ORELSE' (etac notE)
+    then assume_tac ctxt ORELSE' (etac notE)
     else K no_tac);
 *}
 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -2471,7 +2471,7 @@
         fun distinct_prems ctxt thm =
           Goal.prove (*no sorry*) ctxt [] []
             (thm |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies)
-            (fn _ => HEADGOAL (cut_tac thm THEN' atac) THEN ALLGOALS eq_assume_tac);
+            (fn _ => HEADGOAL (cut_tac thm THEN' assume_tac ctxt) THEN ALLGOALS eq_assume_tac);
 
         fun eq_ifIN _ [thm] = thm
           | eq_ifIN ctxt (thm :: thms) =
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -44,7 +44,7 @@
       (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN'
          REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos,
            SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac @{thm order_refl},
-           atac, resolve_tac co_inducts,
+           assume_tac ctxt, resolve_tac co_inducts,
            resolve_tac C_IH_monos THEN' REPEAT_ALL_NEW (eresolve_tac nesting_rel_monos)])))
     co_inducts)
   end;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -452,7 +452,7 @@
         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
       in
         Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
-          (K ((hyp_subst_tac lthy THEN' atac) 1))
+          (K ((hyp_subst_tac lthy THEN' assume_tac lthy) 1))
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
@@ -550,7 +550,7 @@
         val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
       in
         Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
-          (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' atac) 1)
+          (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -394,7 +394,7 @@
         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
       in
         Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
-          (K ((hyp_subst_tac lthy THEN' atac) 1))
+          (K ((hyp_subst_tac lthy THEN' assume_tac lthy) 1))
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -906,7 +906,7 @@
                   val thms =
                     @{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
                         Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
-                          mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac)
+                          mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL (assume_tac ctxt))
                         |> Thm.close_derivation
                         |> not triv ? perhaps (try (fn thm => refl RS thm)))
                       ms discD_thms sel_thmss trivs goals;
--- a/src/HOL/Tools/Function/function_core.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -683,7 +683,7 @@
       subset_induct_rule
       |> Thm.forall_intr (cterm_of thy D)
       |> Thm.forall_elim (cterm_of thy acc_R)
-      |> assume_tac 1 |> Seq.hd
+      |> atac 1 |> Seq.hd
       |> (curry op COMP) (acc_downward
         |> (instantiate' [SOME (ctyp_of thy domT)]
              (map (SOME o cterm_of thy) [R, x, z]))
--- a/src/HOL/Tools/Function/function_elims.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -125,7 +125,7 @@
           REPEAT (eresolve_tac @{thms Pair_inject} i)
           THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
           THEN propagate_tac ctxt i
-          THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
+          THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i)
           THEN bool_subst_tac ctxt i;
 
       val elim_stripped =
--- a/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -396,6 +396,6 @@
 
 
 fun induction_schema_tac ctxt =
-  mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
+  mk_ind_tac (K all_tac) (assume_tac ctxt APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
 
 end
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -32,8 +32,8 @@
   in
     EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]), 
       REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]),
-      rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
-        [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac,
+      rtac rel_mono THEN_ALL_NEW assume_tac ctxt, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
+        [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW assume_tac ctxt,
       SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]),
       hyp_subst_tac ctxt, rtac refl] i
   end
--- a/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -30,8 +30,8 @@
   val make_clauses_unsorted: Proof.context -> thm list -> thm list
   val make_clauses: Proof.context -> thm list -> thm list
   val make_horns: thm list -> thm list
-  val best_prolog_tac: (thm -> int) -> thm list -> tactic
-  val depth_prolog_tac: thm list -> tactic
+  val best_prolog_tac: Proof.context -> (thm -> int) -> thm list -> tactic
+  val depth_prolog_tac: Proof.context -> thm list -> tactic
   val gocls: thm list -> thm list
   val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
   val MESON:
@@ -503,8 +503,8 @@
 
 
 (* net_resolve_tac actually made it slower... *)
-fun prolog_step_tac horns i =
-    (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
+fun prolog_step_tac ctxt horns i =
+    (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN
     TRYALL_eq_assume_tac;
 
 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
@@ -690,11 +690,11 @@
 (*Could simply use nprems_of, which would count remaining subgoals -- no
   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
 
-fun best_prolog_tac sizef horns =
-    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
+fun best_prolog_tac ctxt sizef horns =
+    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1);
 
-fun depth_prolog_tac horns =
-    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
+fun depth_prolog_tac ctxt horns =
+    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1);
 
 (*Return all negative clauses, as possible goal clauses*)
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
@@ -723,7 +723,7 @@
     (fn cls =>
          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
                          (has_fewer_prems 1, sizef)
-                         (prolog_step_tac (make_horns cls) 1))
+                         (prolog_step_tac ctxt (make_horns cls) 1))
     ctxt
 
 (*First, breaks the goal into independent units*)
@@ -734,7 +734,7 @@
 
 fun depth_meson_tac ctxt =
   MESON all_tac (make_clauses ctxt)
-    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)])
+    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)])
     ctxt
 
 (** Iterative deepening version **)
@@ -747,7 +747,7 @@
         val nrtac = net_resolve_tac horns
     in  fn i => eq_assume_tac i ORELSE
                 match_tac ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
-                ((assume_tac i APPEND nrtac i) THEN check_tac)
+                ((assume_tac ctxt i APPEND nrtac i) THEN check_tac)
     end;
 
 fun iter_deepen_prolog_tac ctxt horns =
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -439,7 +439,10 @@
         val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
         val goal = Logic.list_implies (prems, concl)
         val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
-        val tac = cut_tac th 1 THEN rewrite_goals_tac ctxt' meta_not_not THEN ALLGOALS assume_tac
+        val tac =
+          cut_tac th 1 THEN
+          rewrite_goals_tac ctxt' meta_not_not THEN
+          ALLGOALS (assume_tac ctxt')
       in
         if length prems = length prems0 then
           raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
@@ -746,7 +749,7 @@
             THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
               THEN rotate_tac (rotation_of_subgoal i) i
               THEN PRIMITIVE (unify_first_prem_with_concl thy i)
-              THEN assume_tac i
+              THEN assume_tac ctxt' i
               THEN flexflex_tac ctxt')))
       handle ERROR msg =>
         cat_error msg
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -382,8 +382,8 @@
                    (map (pair "x") Ts, S $ Old_Datatype_Aux.app_bnds f i)),
                  HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
                    (r $ (a $ Old_Datatype_Aux.app_bnds f i)), f))))
-              (fn _ => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
-                 REPEAT (etac allE 1), rtac thm 1, atac 1])
+              (fn {context = ctxt, ...} => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
+                 REPEAT (etac allE 1), rtac thm 1, assume_tac ctxt 1])
           end
       in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
 
@@ -431,12 +431,12 @@
                        [REPEAT (eresolve_tac (Scons_inject ::
                           map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
                         REPEAT (cong_tac ctxt 1), rtac refl 1,
-                        REPEAT (atac 1 ORELSE (EVERY
+                        REPEAT (assume_tac ctxt 1 ORELSE (EVERY
                           [REPEAT (rtac @{thm ext} 1),
                            REPEAT (eresolve_tac (mp :: allE ::
                              map make_elim (Suml_inject :: Sumr_inject ::
                                Lim_inject :: inj_thms') @ fun_congs) 1),
-                           atac 1]))])])])]);
+                           assume_tac ctxt 1]))])])])]);
 
         val inj_thms'' = map (fn r => r RS datatype_injI) (Old_Datatype_Aux.split_conj_thm inj_thm);
 
@@ -565,7 +565,7 @@
              REPEAT (eresolve_tac inj_thms 1),
              REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1),
                REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
-               atac 1]))])
+               assume_tac ctxt 1]))])
       end;
 
     val constr_inject =
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -183,7 +183,7 @@
                 REPEAT_DETERM_N j distinct_tac,
                 TRY (dresolve_tac inject 1),
                 REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1,
-                REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac 1]),
+                REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac ctxt 1]),
                 TRY (hyp_subst_tac ctxt 1),
                 resolve_tac [refl] 1,
                 REPEAT_DETERM_N (n - j - 1) distinct_tac],
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -171,8 +171,8 @@
               THEN EVERY1 (select_disj (length disjuncts) (index + 1)) 
               THEN (EVERY (map (fn y =>
                 rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
-              THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
-              THEN TRY (atac 1)
+              THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
+              THEN TRY (assume_tac ctxt' 1)
           in
             Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac)
           end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -78,7 +78,7 @@
     THEN trace_tac ctxt options "prove_param"
     THEN f_tac
     THEN trace_tac ctxt options "after prove_param"
-    THEN (REPEAT_DETERM (atac 1))
+    THEN (REPEAT_DETERM (assume_tac ctxt 1))
     THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
     THEN REPEAT_DETERM (rtac @{thm refl} 1)
   end
@@ -97,11 +97,11 @@
         THEN trace_tac ctxt options "after intro rule"
         (* for the right assumption in first position *)
         THEN rotate_tac premposition 1
-        THEN atac 1
+        THEN assume_tac ctxt 1
         THEN trace_tac ctxt options "parameter goal"
         (* work with parameter arguments *)
         THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
-        THEN (REPEAT_DETERM (atac 1))
+        THEN (REPEAT_DETERM (assume_tac ctxt 1))
       end
   | (Free _, _) =>
       trace_tac ctxt options "proving parameter call.."
@@ -242,7 +242,7 @@
                       THEN rtac (nth prems premposition) 1) ctxt 1
                     THEN trace_tac ctxt options "after applying not introduction rule"
                     THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
-                    THEN (REPEAT_DETERM (atac 1))
+                    THEN (REPEAT_DETERM (assume_tac ctxt 1))
                   else
                     rtac @{thm not_predI'} 1
                     (* test: *)
@@ -410,8 +410,10 @@
         THEN (rtac pred_intro_rule
         (* How to handle equality correctly? *)
         THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
-        THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac)))
-          THEN' (K (trace_tac ctxt options "state after pre-simplification:"))
+        THEN' (assume_tac ctxt ORELSE'
+          ((CHANGED o asm_full_simp_tac split_simpset) THEN'
+            (TRY o assume_tac ctxt))) THEN'
+          (K (trace_tac ctxt options "state after pre-simplification:"))
         THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1))
     | prove_prems2 out_ts ((p, deriv) :: ps) =
       let
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -396,7 +396,7 @@
                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
 
     (* resolving with R x y assumptions *)
-    atac,
+    assume_tac ctxt,
 
     (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
     rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
@@ -560,7 +560,7 @@
       val concl' = apply_under_Trueprop (all_list vrs) concl
       val goal = Logic.mk_implies (concl', concl)
       val rule = Goal.prove ctxt [] [] goal
-        (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
+        (K (EVERY1 [inst_spec_tac (rev cvrs), assume_tac ctxt]))
     in
       rtac rule i
     end)
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -51,7 +51,7 @@
 
 
 (* tactic to prove the quot_type theorem for the new type *)
-fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
+fun typedef_quot_type_tac ctxt equiv_thm ((_, typedef_info): Typedef.info) =
   let
     val rep_thm = #Rep typedef_info RS mem_def1
     val rep_inv = #Rep_inverse typedef_info
@@ -62,7 +62,7 @@
       rtac equiv_thm,
       rtac rep_thm,
       rtac rep_inv,
-      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
+      rtac abs_inv THEN' rtac mem_def2 THEN' assume_tac ctxt,
       rtac rep_inj]) 1
   end
 
@@ -74,7 +74,7 @@
     val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
   in
     Goal.prove lthy [] [] goal
-      (K (typedef_quot_type_tac equiv_thm typedef_info))
+      (fn {context = ctxt, ...} => typedef_quot_type_tac ctxt equiv_thm typedef_info)
   end
    
 open Lifting_Util
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -78,12 +78,13 @@
       rel_OO_of_bnf bnf]
   in
     (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
-      THEN_ALL_NEW atac) i
+      THEN_ALL_NEW assume_tac ctxt) i
   end
 
 fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
   (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
-    CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
+    CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW
+      (REPEAT_DETERM o etac conjE THEN' assume_tac ctxt)) sided_constr_intros) i
 
 fun generate_relation_constraint_goal ctxt bnf constraint_def =
   let
@@ -199,7 +200,8 @@
         in_rel_of_bnf bnf, pred_def]), rtac iffI,
         REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
         CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
-          etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
+          etac imageE, dtac set_rev_mp, assume_tac ctxt,
+          REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
           hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
           etac @{thm DomainPI}]) set_map's,
         REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
@@ -209,7 +211,8 @@
           rtac @{thm fst_conv}]), rtac CollectI,
         CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
           REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
-          dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
+          dtac (rotate_prems 1 bspec), assume_tac ctxt,
+          etac @{thm DomainpE}, etac @{thm someI}]) set_map's
       ] i
   end
 
--- a/src/HOL/Tools/cnf.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/cnf.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -42,7 +42,7 @@
   val clause2raw_thm: thm -> thm
   val make_nnf_thm: theory -> term -> thm
 
-  val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
+  val weakening_tac: Proof.context -> int -> tactic  (* removes the first hypothesis of a subgoal *)
 
   val make_cnf_thm: Proof.context -> term -> thm
   val make_cnfx_thm: Proof.context -> term -> thm
@@ -528,8 +528,8 @@
 (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
 (* ------------------------------------------------------------------------- *)
 
-fun weakening_tac i =
-  dresolve_tac [weakening_thm] i THEN assume_tac (i+1);
+fun weakening_tac ctxt i =
+  dresolve_tac [weakening_thm] i THEN assume_tac ctxt (i+1);
 
 (* ------------------------------------------------------------------------- *)
 (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
@@ -551,7 +551,7 @@
     let
       val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
     in
-      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
+      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac ctxt 1)) thm
     end) i;
 
 (* ------------------------------------------------------------------------- *)
@@ -573,7 +573,7 @@
     let
       val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
     in
-      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
+      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac ctxt 1)) thm
     end) i;
 
 end;
--- a/src/HOL/Tools/datatype_realizer.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -118,7 +118,7 @@
             ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
             rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
             REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
-              REPEAT (etac allE i) THEN atac i)) 1)])
+              REPEAT (etac allE i) THEN assume_tac ctxt i)) 1)])
       |> Drule.export_without_context;
 
     val ind_name = Thm.derivation_name induct;
--- a/src/HOL/Tools/inductive.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -381,7 +381,7 @@
     (fn _ => EVERY [resolve_tac @{thms monoI} 1,
       REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
       REPEAT (FIRST
-        [assume_tac 1,
+        [assume_tac ctxt 1,
          resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
          eresolve_tac @{thms le_funE} 1,
          dresolve_tac @{thms le_boolD} 1])]));
@@ -406,7 +406,7 @@
         EVERY1 (select_disj (length intr_ts) (i + 1)),
         (*Not ares_tac, since refl must be tried before any equality assumptions;
           backtracking may occur if the premises have extra variables!*)
-        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
+        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac ctxt 1)])
        |> singleton (Proof_Context.export ctxt ctxt')) intr_ts
 
   in (intrs, unfold) end;
@@ -544,7 +544,7 @@
 
 (*delete needless equality assumptions*)
 val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
-  (fn _ => assume_tac 1);
+  (fn {context = ctxt, ...} => assume_tac ctxt 1);
 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
 val elim_tac = REPEAT o eresolve_tac elim_rls;
 
@@ -741,7 +741,7 @@
            some premise involves disjunction.*)
          REPEAT (FIRSTGOAL (eresolve_tac [conjE] ORELSE' bound_hyp_subst_tac ctxt3)),
          REPEAT (FIRSTGOAL
-           (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac))),
+           (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac ctxt3))),
          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
              (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
            conjI, refl] 1)) prems)]);
@@ -752,9 +752,9 @@
          REPEAT (EVERY
            [REPEAT (resolve_tac [conjI, impI] 1),
             REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
-            assume_tac 1,
+            assume_tac ctxt3 1,
             rewrite_goals_tac ctxt3 simp_thms1,
-            assume_tac 1])]);
+            assume_tac ctxt3 1])]);
 
   in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
 
--- a/src/HOL/Tools/inductive_realizer.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -397,7 +397,7 @@
            rewrite_goals_tac ctxt rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
              [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
-              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
+              DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE]]) 1)]);
         val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
           (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
@@ -460,7 +460,7 @@
              ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
              rewrite_goals_tac ctxt rews,
              REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
-               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
+               DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE])) 1)]);
         val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
           (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
       in
--- a/src/HOL/Tools/record.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/record.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -1625,9 +1625,9 @@
         (fn {context = ctxt, ...} =>
           EVERY1
            [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
-            etac @{thm meta_allE}, atac,
+            etac @{thm meta_allE}, assume_tac ctxt,
             rtac (@{thm prop_subst} OF [surject]),
-            REPEAT o etac @{thm meta_allE}, atac]));
+            REPEAT o etac @{thm meta_allE}, assume_tac ctxt]));
 
     val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
       let val (assm, concl) = induct_prop in
@@ -2160,9 +2160,9 @@
         (fn {context = ctxt', ...} =>
           EVERY1
            [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
-            etac @{thm meta_allE}, atac,
+            etac @{thm meta_allE}, assume_tac ctxt',
             rtac (@{thm prop_subst} OF [surjective]),
-            REPEAT o etac @{thm meta_allE}, atac]));
+            REPEAT o etac @{thm meta_allE}, assume_tac ctxt']));
 
     val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
       Goal.prove_sorry_global defs_thy [] [] split_object_prop
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -344,7 +344,7 @@
     THEN' resolve_tac @{thms UnI2}
     THEN' tac1_of_formula ctxt fm2
   | tac1_of_formula ctxt (Atom _) =
-    REPEAT_DETERM1 o (assume_tac
+    REPEAT_DETERM1 o (assume_tac ctxt
       ORELSE' resolve_tac @{thms SigmaI}
       ORELSE' ((resolve_tac @{thms CollectI} ORELSE' resolve_tac [collectI']) THEN'
         TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
@@ -356,7 +356,7 @@
       ORELSE' resolve_tac @{thms arg_cong2[OF refl, where f = "op =", OF prod.case, THEN iffD2]})))
       ORELSE' resolve_tac @{thms UNIV_I}
       ORELSE' resolve_tac @{thms iffD2[OF Compl_iff]}
-      ORELSE' assume_tac)
+      ORELSE' assume_tac ctxt)
 
 fun tac2_of_formula ctxt (Int (fm1, fm2)) =
     TRY o eresolve_tac @{thms IntE}
@@ -370,7 +370,7 @@
     THEN' tac2_of_formula ctxt fm2
   | tac2_of_formula ctxt (Atom _) =
     REPEAT_DETERM o
-      (assume_tac
+      (assume_tac ctxt
        ORELSE' dresolve_tac @{thms iffD1[OF mem_Sigma_iff]}
        ORELSE' eresolve_tac @{thms conjE}
        ORELSE' ((eresolve_tac @{thms CollectE} ORELSE' eresolve_tac [collectE']) THEN'
@@ -434,14 +434,14 @@
       THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
       THEN' resolve_tac @{thms iffI}
       THEN' REPEAT_DETERM o resolve_tac @{thms exI}
-      THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac
+      THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac ctxt
       THEN' REPEAT_DETERM o eresolve_tac @{thms exE}
       THEN' eresolve_tac @{thms conjE}
       THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
       THEN' Subgoal.FOCUS (fn {prems, ...} =>
         (* FIXME inner context!? *)
         simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
-      THEN' TRY o assume_tac
+      THEN' TRY o assume_tac ctxt
   in
     case try mk_term (term_of ct) of
       NONE => Thm.reflexive ct
--- a/src/HOL/Tools/simpdata.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -119,7 +119,7 @@
     val sol_thms =
       reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
     fun sol_tac i =
-      FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
+      FIRST [resolve_tac sol_thms i, assume_tac ctxt i , eresolve_tac @{thms FalseE} i] ORELSE
       (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
   in
     (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
--- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -713,7 +713,7 @@
   EVERY [
     simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
     rtac @{thm guarantees_PLam_I} 1,
-    assume_tac 2,
+    assume_tac ctxt 2,
          (*preserves: routine reasoning*)
     asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2,
          (*the guarantee for  "lift i (rename client_map Client)" *)
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -110,7 +110,7 @@
       full_simp_tac ctxt 1,
       REPEAT (FIRSTGOAL (etac disjE)),
       ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])),
-      REPEAT (FIRSTGOAL analz_mono_contra_tac),
+      REPEAT (FIRSTGOAL (analz_mono_contra_tac ctxt)),
       ALLGOALS (asm_simp_tac ctxt)]) i;
 
 (*Tactic for proving secrecy theorems*)
--- a/src/HOL/UNITY/UNITY_tactics.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -6,7 +6,8 @@
 *)
 
 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
-val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
+fun Always_Int_tac ctxt =
+  dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin}
 
 (*Combines a list of invariance THEOREMS into one.*)
 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
@@ -16,7 +17,7 @@
 fun constrains_tac ctxt i =
   SELECT_GOAL
     (EVERY
-     [REPEAT (Always_Int_tac 1),
+     [REPEAT (Always_Int_tac ctxt 1),
       (*reduce the fancy safety properties to "constrains"*)
       REPEAT (etac @{thm Always_ConstrainsI} 1
               ORELSE
@@ -35,7 +36,7 @@
 fun ensures_tac ctxt sact =
   SELECT_GOAL
     (EVERY
-     [REPEAT (Always_Int_tac 1),
+     [REPEAT (Always_Int_tac ctxt 1),
       etac @{thm Always_LeadsTo_Basis} 1
           ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
           REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
--- a/src/HOL/Word/Word.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Word/Word.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -1565,8 +1565,8 @@
       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
                          REPEAT (etac conjE n) THEN
                          REPEAT (dtac @{thm word_of_int_inverse} n 
-                                 THEN atac n 
-                                 THEN atac n)),
+                                 THEN assume_tac ctxt n 
+                                 THEN assume_tac ctxt n)),
       TRYALL arith_tac' ]
   end
 
--- a/src/HOL/ex/Meson_Test.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/ex/Meson_Test.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -40,7 +40,7 @@
     val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       rtac go25 1 THEN
-      Meson.depth_prolog_tac horns25);
+      Meson.depth_prolog_tac ctxt' horns25);
   *}
   oops
 
@@ -66,7 +66,7 @@
     val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       rtac go26 1 THEN
-      Meson.depth_prolog_tac horns26);  (*7 ms*)
+      Meson.depth_prolog_tac ctxt' horns26);  (*7 ms*)
     (*Proof is of length 107!!*)
   *}
   oops
@@ -93,7 +93,7 @@
     val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
     Goal.prove ctxt' [] [] @{prop False} (fn _ =>
       rtac go43 1 THEN
-      Meson.best_prolog_tac Meson.size_of_subgoals horns43);   (*7ms*)
+      Meson.best_prolog_tac ctxt' Meson.size_of_subgoals horns43);   (*7ms*)
     *}
   oops
 
--- a/src/Provers/blast.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Provers/blast.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -782,14 +782,14 @@
 
 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
 fun contr_tac ctxt =
-  ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac);
+  ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac ctxt);
 
 (*Try to unify complementary literals and return the corresponding tactic. *)
 fun tryClose state (G, L) =
   let
     val State {ctxt, ...} = state;
     val eContr_tac = TRACE ctxt Data.notE contr_tac;
-    val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac);
+    val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac ctxt);
     fun close t u tac = if unify state ([], t, u) then SOME tac else NONE;
     fun arg (_ $ t) = t;
   in
--- a/src/Provers/classical.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Provers/classical.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -71,14 +71,14 @@
   val depth_tac: Proof.context -> int -> int -> tactic
   val deepen_tac: Proof.context -> int -> int -> tactic
 
-  val contr_tac: int -> tactic
+  val contr_tac: Proof.context -> int -> tactic
   val dup_elim: Context.generic option -> thm -> thm
   val dup_intr: thm -> thm
   val dup_step_tac: Proof.context -> int -> tactic
   val eq_mp_tac: Proof.context -> int -> tactic
   val haz_step_tac: Proof.context -> int -> tactic
   val joinrules: thm list * thm list -> (bool * thm) list
-  val mp_tac: int -> tactic
+  val mp_tac: Proof.context -> int -> tactic
   val safe_tac: Proof.context -> tactic
   val safe_steps_tac: Proof.context -> int -> tactic
   val safe_step_tac: Proof.context -> int -> tactic
@@ -87,7 +87,7 @@
   val step_tac: Proof.context -> int -> tactic
   val slow_step_tac: Proof.context -> int -> tactic
   val swapify: thm list -> thm list
-  val swap_res_tac: thm list -> int -> tactic
+  val swap_res_tac: Proof.context -> thm list -> int -> tactic
   val inst_step_tac: Proof.context -> int -> tactic
   val inst0_step_tac: Proof.context -> int -> tactic
   val instp_step_tac: Proof.context -> int -> tactic
@@ -179,12 +179,12 @@
 (*Prove goal that assumes both P and ~P.
   No backtracking if it finds an equal assumption.  Perhaps should call
   ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
-val contr_tac =
-  eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac);
+fun contr_tac ctxt =
+  eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt);
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   Could do the same thing for P<->Q and P... *)
-fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
+fun mp_tac ctxt i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i;
 
 (*Like mp_tac but instantiates no variables*)
 fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
@@ -195,10 +195,10 @@
 
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
-fun swap_res_tac rls =
+fun swap_res_tac ctxt rls =
   let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in
-    assume_tac ORELSE'
-    contr_tac ORELSE'
+    assume_tac ctxt ORELSE'
+    contr_tac ctxt ORELSE'
     biresolve_tac (fold_rev addrl rls [])
   end;
 
@@ -693,9 +693,9 @@
   ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
 
 fun ctxt addD2 (name, thm) =
-  ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
+  ctxt addafter (name, fn ctxt' => dresolve_tac [thm] THEN' assume_tac ctxt');
 fun ctxt addE2 (name, thm) =
-  ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
+  ctxt addafter (name, fn ctxt' => eresolve_tac [thm] THEN' assume_tac ctxt');
 fun ctxt addSD2 (name, thm) =
   ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac);
 fun ctxt addSE2 (name, thm) =
@@ -762,8 +762,8 @@
 (*Backtracking is allowed among the various these unsafe ways of
   proving a subgoal.  *)
 fun inst0_step_tac ctxt =
-  assume_tac APPEND'
-  contr_tac APPEND'
+  assume_tac ctxt APPEND'
+  contr_tac ctxt APPEND'
   biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
 
 (*These unsafe steps could generate more subgoals.*)
--- a/src/Provers/typedsimp.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Provers/typedsimp.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -18,19 +18,19 @@
   (*Built-in rewrite rules*)
   val default_rls: thm list
   (*Type checking or similar -- solution of routine conditions*)
-  val routine_tac: thm list -> int -> tactic
+  val routine_tac: Proof.context -> thm list -> int -> tactic
   end;
 
 signature TSIMP =
   sig
-  val asm_res_tac: thm list -> int -> tactic   
-  val cond_norm_tac: ((int->tactic) * thm list * thm list) -> tactic
-  val cond_step_tac: ((int->tactic) * thm list * thm list) -> int -> tactic
-  val norm_tac: (thm list * thm list) -> tactic
+  val asm_res_tac: Proof.context -> thm list -> int -> tactic   
+  val cond_norm_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> tactic
+  val cond_step_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> int -> tactic
+  val norm_tac: Proof.context -> (thm list * thm list) -> tactic
   val process_rules: thm list -> thm list * thm list
   val rewrite_res_tac: int -> tactic   
   val split_eqn: thm
-  val step_tac: (thm list * thm list) -> int -> tactic
+  val step_tac: Proof.context -> (thm list * thm list) -> int -> tactic
   val subconv_res_tac: thm list -> int -> tactic   
   end;
 
@@ -95,29 +95,29 @@
   ORELSE'  filt_resolve_tac [refl,refl_red] 1;
 
 (*Resolve with asms, whether rewrites or not*)
-fun asm_res_tac asms =
+fun asm_res_tac ctxt asms =
     let val (xsimp_rls,xother_rls) = process_rules asms
-    in  routine_tac xother_rls  ORELSE'  
+    in  routine_tac ctxt xother_rls  ORELSE'  
         filt_resolve_tac xsimp_rls 2
     end;
 
 (*Single step for simple rewriting*)
-fun step_tac (congr_rls,asms) =
-    asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
+fun step_tac ctxt (congr_rls,asms) =
+    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac  ORELSE'  
     subconv_res_tac congr_rls;
 
 (*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)
-fun cond_step_tac (prove_cond_tac, congr_rls, asms) =
-    asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
+fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) =
+    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac  ORELSE'  
     (resolve_tac [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'  
     subconv_res_tac congr_rls;
 
 (*Unconditional normalization tactic*)
-fun norm_tac arg = REPEAT_FIRST (step_tac arg)  THEN
+fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg)  THEN
     TRYALL (resolve_tac [red_if_equal]);
 
 (*Conditional normalization tactic*)
-fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg)  THEN
+fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg)  THEN
     TRYALL (resolve_tac [red_if_equal]);
 
 end;
--- a/src/Pure/Isar/class_declaration.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -97,7 +97,7 @@
     fun tac ctxt =
       REPEAT (SOMEGOAL
         (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
-          ORELSE' assume_tac));
+          ORELSE' assume_tac ctxt));
     val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
 
   in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
--- a/src/Pure/Isar/method.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/Isar/method.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -167,7 +167,7 @@
 in
 
 fun assm_tac ctxt =
-  assume_tac APPEND'
+  assume_tac ctxt APPEND'
   Goal.assume_rule_tac ctxt APPEND'
   cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
   cond_rtac (can Logic.dest_term) Drule.termI;
@@ -211,7 +211,7 @@
   THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
 
 fun gen_arule_tac tac ctxt j rules facts =
-  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac);
+  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt));
 
 fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) =>
   let
--- a/src/Pure/Tools/rule_insts.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -301,7 +301,7 @@
 fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve ctxt rule);
 
 (*forward tactic applies a rule to an assumption without deleting it*)
-fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
+fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac ctxt;
 
 (*dresolve tactic applies a rule to replace an assumption*)
 fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve ctxt rule);
--- a/src/Pure/goal.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/goal.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -336,7 +336,7 @@
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
     val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
     val tacs = Rs |> map (fn R =>
-      eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac);
+      eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt);
   in fold_rev (curry op APPEND') tacs (K no_tac) i end);
 
 end;
--- a/src/Pure/simplifier.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/simplifier.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -384,7 +384,7 @@
     val trivialities = Drule.reflexive_thm :: trivs;
 
     fun unsafe_solver_tac ctxt =
-      FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac];
+      FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
     val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
 
     (*no premature instantiation of variables during simplification*)
--- a/src/Pure/tactic.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Pure/tactic.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -8,7 +8,7 @@
 sig
   val trace_goalno_tac: (int -> tactic) -> int -> tactic
   val rule_by_tactic: Proof.context -> tactic -> thm -> thm
-  val assume_tac: int -> tactic
+  val assume_tac: Proof.context -> int -> tactic
   val eq_assume_tac: int -> tactic
   val compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic
   val make_elim: thm -> thm
@@ -101,7 +101,8 @@
      thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
 
 (*Solve subgoal i by assumption*)
-fun assume_tac i = PRIMSEQ (Thm.assumption NONE i);
+fun assume_tac ctxt i = PRIMSEQ (Thm.assumption (SOME ctxt) i);
+fun atac i = PRIMSEQ (Thm.assumption NONE i);
 
 (*Solve subgoal i by assumption, using no unification*)
 fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
@@ -128,22 +129,21 @@
 fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
 
 (*Forward reasoning using destruction rules.*)
-fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
+fun forward_tac rls = resolve_tac (map make_elim rls) THEN' atac;
 
 (*Like forward_tac, but deletes the assumption after use.*)
 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
 
 (*Shorthand versions: for resolution with a single theorem*)
-val atac    =   assume_tac;
 fun rtac rl =  resolve_tac [rl];
 fun dtac rl = dresolve_tac [rl];
 fun etac rl = eresolve_tac [rl];
 fun ftac rl =  forward_tac [rl];
 
 (*Use an assumption or some rules ... A popular combination!*)
-fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
+fun ares_tac rules = atac  ORELSE'  resolve_tac rules;
 
-fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
+fun solve_tac rules = resolve_tac rules THEN_ALL_NEW atac;
 
 (*Matching tactics -- as above, but forbid updating of state*)
 fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i);
--- a/src/Sequents/simpdata.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Sequents/simpdata.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -58,7 +58,7 @@
   @{thm iff_refl}, reflexive_thm];
 
 fun unsafe_solver ctxt =
-  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac];
+  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt];
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver ctxt =
--- a/src/Tools/intuitionistic.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Tools/intuitionistic.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -34,7 +34,7 @@
 
 fun unsafe_step_tac ctxt =
   Context_Rules.wrap ctxt
-   (assume_tac APPEND'
+   (assume_tac ctxt APPEND'
     bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
     bires_tac false (Context_Rules.netpair ctxt));
 
--- a/src/ZF/Tools/inductive_package.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -220,7 +220,7 @@
      resolve_tac [disjIn] 2,
      (*Not ares_tac, since refl must be tried before equality assumptions;
        backtracking may occur if the premises have extra variables!*)
-     DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
+     DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac ctxt 2),
      (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
      rewrite_goals_tac ctxt con_defs,
      REPEAT (resolve_tac @{thms refl} 2),
@@ -233,7 +233,7 @@
                         ORELSE' hyp_subst_tac ctxt1)),
      if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:"
      else all_tac,
-     DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
+     DEPTH_SOLVE (swap_res_tac ctxt (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
 
   (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
   val mk_disj_rls = Balanced_Tree.accesses
@@ -330,7 +330,7 @@
              |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
            setSolver (mk_solver "minimal"
                       (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)
-                                   ORELSE' assume_tac
+                                   ORELSE' assume_tac ctxt
                                    ORELSE' eresolve_tac @{thms FalseE}));
 
      val quant_induct =
--- a/src/ZF/Tools/typechk.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/ZF/Tools/typechk.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -81,16 +81,17 @@
   | is_rigid_elem _ = false;
 
 (*Try solving a:A by assumption provided a is rigid!*)
-val test_assume_tac = SUBGOAL(fn (prem,i) =>
+fun test_assume_tac ctxt = SUBGOAL(fn (prem,i) =>
     if is_rigid_elem (Logic.strip_assums_concl prem)
-    then  assume_tac i  else  eq_assume_tac i);
+    then  assume_tac ctxt i  else  eq_assume_tac i);
 
 (*Type checking solves a:?A (a rigid, ?A maybe flexible).
   match_tac is too strict; would refuse to instantiate ?A*)
-fun typecheck_step_tac (TC{net,...}) =
-    FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
+fun typecheck_step_tac ctxt =
+  let val TC {net, ...} = tcset_of ctxt
+  in FIRSTGOAL (test_assume_tac ctxt ORELSE' net_res_tac 3 net) end;
 
-fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt));
+fun typecheck_tac ctxt = REPEAT (typecheck_step_tac ctxt);
 
 (*Compiles a term-net for speed*)
 val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl},
@@ -102,7 +103,7 @@
     (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
                   ORELSE basic_res_tac 1
                   ORELSE (ares_tac hyps 1
-                          APPEND typecheck_step_tac (tcset_of ctxt))));
+                          APPEND typecheck_step_tac ctxt)));
 
 val type_solver =
   Simplifier.mk_solver "ZF typecheck" (fn ctxt =>
--- a/src/ZF/UNITY/Constrains.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/ZF/UNITY/Constrains.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -459,7 +459,8 @@
 ML
 {*
 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
-val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin};
+fun Always_Int_tac ctxt =
+  dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin};
 
 (*Combines a list of invariance THEOREMS into one.*)
 val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
@@ -468,7 +469,7 @@
 
 fun constrains_tac ctxt =
    SELECT_GOAL
-      (EVERY [REPEAT (Always_Int_tac 1),
+      (EVERY [REPEAT (Always_Int_tac ctxt 1),
               REPEAT (etac @{thm Always_ConstrainsI} 1
                       ORELSE
                       resolve_tac [@{thm StableI}, @{thm stableI},
--- a/src/ZF/UNITY/SubstAx.thy	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/ZF/UNITY/SubstAx.thy	Mon Nov 10 21:49:48 2014 +0100
@@ -352,7 +352,7 @@
 (*proves "ensures/leadsTo" properties when the program is specified*)
 fun ensures_tac ctxt sact =
   SELECT_GOAL
-    (EVERY [REPEAT (Always_Int_tac 1),
+    (EVERY [REPEAT (Always_Int_tac ctxt 1),
             etac @{thm Always_LeadsTo_Basis} 1
                 ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
                 REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},