proper context for assume_tac (atac remains as fall-back without context);
authorwenzelm
Mon Nov 10 21:49:48 2014 +0100 (2014-11-10)
changeset 5896326bf09b95dda
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
     1.1 --- a/NEWS	Sun Nov 09 20:49:28 2014 +0100
     1.2 +++ b/NEWS	Mon Nov 10 21:49:48 2014 +0100
     1.3 @@ -190,8 +190,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 -* Proper context for various elementary tactics: match_tac, compose_tac,
     1.8 -Splitter.split_tac etc.  Minor INCOMPATIBILITY.
     1.9 +* Proper context for various elementary tactics: assume_tac,
    1.10 +match_tac, compose_tac, Splitter.split_tac etc.  Minor
    1.11 +INCOMPATIBILITY.
    1.12  
    1.13  * Tactical PARALLEL_ALLGOALS is the most common way to refer to
    1.14  PARALLEL_GOALS.
     2.1 --- a/src/CCL/Wfd.thy	Sun Nov 09 20:49:28 2014 +0100
     2.2 +++ b/src/CCL/Wfd.thy	Mon Nov 10 21:49:48 2014 +0100
     2.3 @@ -48,7 +48,7 @@
     2.4  
     2.5  ML {*
     2.6    fun wfd_strengthen_tac ctxt s i =
     2.7 -    res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1)
     2.8 +    res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i+1)
     2.9  *}
    2.10  
    2.11  lemma wf_anti_sym: "[| Wfd(r);  <a,x>:r;  <x,a>:r |] ==> P"
     3.1 --- a/src/CTT/Arith.thy	Sun Nov 09 20:49:28 2014 +0100
     3.2 +++ b/src/CTT/Arith.thy	Mon Nov 10 21:49:48 2014 +0100
     3.3 @@ -54,12 +54,12 @@
     3.4  
     3.5  lemma add_typing: "[| a:N;  b:N |] ==> a #+ b : N"
     3.6  apply (unfold arith_defs)
     3.7 -apply (tactic "typechk_tac []")
     3.8 +apply (tactic "typechk_tac @{context} []")
     3.9  done
    3.10  
    3.11  lemma add_typingL: "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
    3.12  apply (unfold arith_defs)
    3.13 -apply (tactic "equal_tac []")
    3.14 +apply (tactic "equal_tac @{context} []")
    3.15  done
    3.16  
    3.17  
    3.18 @@ -67,12 +67,12 @@
    3.19  
    3.20  lemma addC0: "b:N ==> 0 #+ b = b : N"
    3.21  apply (unfold arith_defs)
    3.22 -apply (tactic "rew_tac []")
    3.23 +apply (tactic "rew_tac @{context} []")
    3.24  done
    3.25  
    3.26  lemma addC_succ: "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
    3.27  apply (unfold arith_defs)
    3.28 -apply (tactic "rew_tac []")
    3.29 +apply (tactic "rew_tac @{context} []")
    3.30  done
    3.31  
    3.32  
    3.33 @@ -82,24 +82,24 @@
    3.34  
    3.35  lemma mult_typing: "[| a:N;  b:N |] ==> a #* b : N"
    3.36  apply (unfold arith_defs)
    3.37 -apply (tactic {* typechk_tac [@{thm add_typing}] *})
    3.38 +apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *})
    3.39  done
    3.40  
    3.41  lemma mult_typingL: "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
    3.42  apply (unfold arith_defs)
    3.43 -apply (tactic {* equal_tac [@{thm add_typingL}] *})
    3.44 +apply (tactic {* equal_tac @{context} [@{thm add_typingL}] *})
    3.45  done
    3.46  
    3.47  (*computation for mult: 0 and successor cases*)
    3.48  
    3.49  lemma multC0: "b:N ==> 0 #* b = 0 : N"
    3.50  apply (unfold arith_defs)
    3.51 -apply (tactic "rew_tac []")
    3.52 +apply (tactic "rew_tac @{context} []")
    3.53  done
    3.54  
    3.55  lemma multC_succ: "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
    3.56  apply (unfold arith_defs)
    3.57 -apply (tactic "rew_tac []")
    3.58 +apply (tactic "rew_tac @{context} []")
    3.59  done
    3.60  
    3.61  
    3.62 @@ -109,12 +109,12 @@
    3.63  
    3.64  lemma diff_typing: "[| a:N;  b:N |] ==> a - b : N"
    3.65  apply (unfold arith_defs)
    3.66 -apply (tactic "typechk_tac []")
    3.67 +apply (tactic "typechk_tac @{context} []")
    3.68  done
    3.69  
    3.70  lemma diff_typingL: "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
    3.71  apply (unfold arith_defs)
    3.72 -apply (tactic "equal_tac []")
    3.73 +apply (tactic "equal_tac @{context} []")
    3.74  done
    3.75  
    3.76  
    3.77 @@ -122,7 +122,7 @@
    3.78  
    3.79  lemma diffC0: "a:N ==> a - 0 = a : N"
    3.80  apply (unfold arith_defs)
    3.81 -apply (tactic "rew_tac []")
    3.82 +apply (tactic "rew_tac @{context} []")
    3.83  done
    3.84  
    3.85  (*Note: rec(a, 0, %z w.z) is pred(a). *)
    3.86 @@ -130,7 +130,7 @@
    3.87  lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
    3.88  apply (unfold arith_defs)
    3.89  apply (tactic {* NE_tac @{context} "b" 1 *})
    3.90 -apply (tactic "hyp_rew_tac []")
    3.91 +apply (tactic "hyp_rew_tac @{context} []")
    3.92  done
    3.93  
    3.94  
    3.95 @@ -138,9 +138,9 @@
    3.96    succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
    3.97  lemma diff_succ_succ: "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
    3.98  apply (unfold arith_defs)
    3.99 -apply (tactic "hyp_rew_tac []")
   3.100 +apply (tactic "hyp_rew_tac @{context} []")
   3.101  apply (tactic {* NE_tac @{context} "b" 1 *})
   3.102 -apply (tactic "hyp_rew_tac []")
   3.103 +apply (tactic "hyp_rew_tac @{context} []")
   3.104  done
   3.105  
   3.106  
   3.107 @@ -173,11 +173,11 @@
   3.108  
   3.109  local val congr_rls = @{thms congr_rls} in
   3.110  
   3.111 -fun arith_rew_tac prems = make_rew_tac
   3.112 -    (Arith_simp.norm_tac(congr_rls, prems))
   3.113 +fun arith_rew_tac ctxt prems = make_rew_tac ctxt
   3.114 +    (Arith_simp.norm_tac ctxt (congr_rls, prems))
   3.115  
   3.116 -fun hyp_arith_rew_tac prems = make_rew_tac
   3.117 -    (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems))
   3.118 +fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt
   3.119 +    (Arith_simp.cond_norm_tac ctxt (prove_cond_tac, congr_rls, prems))
   3.120  
   3.121  end
   3.122  *}
   3.123 @@ -188,7 +188,7 @@
   3.124  (*Associative law for addition*)
   3.125  lemma add_assoc: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
   3.126  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.127 -apply (tactic "hyp_arith_rew_tac []")
   3.128 +apply (tactic "hyp_arith_rew_tac @{context} []")
   3.129  done
   3.130  
   3.131  
   3.132 @@ -196,11 +196,11 @@
   3.133    Must simplify after first induction!  Orientation of rewrites is delicate*)
   3.134  lemma add_commute: "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
   3.135  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.136 -apply (tactic "hyp_arith_rew_tac []")
   3.137 +apply (tactic "hyp_arith_rew_tac @{context} []")
   3.138  apply (tactic {* NE_tac @{context} "b" 2 *})
   3.139  apply (rule sym_elem)
   3.140  apply (tactic {* NE_tac @{context} "b" 1 *})
   3.141 -apply (tactic "hyp_arith_rew_tac []")
   3.142 +apply (tactic "hyp_arith_rew_tac @{context} []")
   3.143  done
   3.144  
   3.145  
   3.146 @@ -209,32 +209,32 @@
   3.147  (*right annihilation in product*)
   3.148  lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
   3.149  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.150 -apply (tactic "hyp_arith_rew_tac []")
   3.151 +apply (tactic "hyp_arith_rew_tac @{context} []")
   3.152  done
   3.153  
   3.154  (*right successor law for multiplication*)
   3.155  lemma mult_succ_right: "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
   3.156  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.157 -apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
   3.158 +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *})
   3.159  apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
   3.160  done
   3.161  
   3.162  (*Commutative law for multiplication*)
   3.163  lemma mult_commute: "[| a:N;  b:N |] ==> a #* b = b #* a : N"
   3.164  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.165 -apply (tactic {* hyp_arith_rew_tac [@{thm mult_0_right}, @{thm mult_succ_right}] *})
   3.166 +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm mult_0_right}, @{thm mult_succ_right}] *})
   3.167  done
   3.168  
   3.169  (*addition distributes over multiplication*)
   3.170  lemma add_mult_distrib: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
   3.171  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.172 -apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
   3.173 +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *})
   3.174  done
   3.175  
   3.176  (*Associative law for multiplication*)
   3.177  lemma mult_assoc: "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
   3.178  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.179 -apply (tactic {* hyp_arith_rew_tac [@{thm add_mult_distrib}] *})
   3.180 +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_mult_distrib}] *})
   3.181  done
   3.182  
   3.183  
   3.184 @@ -246,7 +246,7 @@
   3.185  
   3.186  lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
   3.187  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.188 -apply (tactic "hyp_arith_rew_tac []")
   3.189 +apply (tactic "hyp_arith_rew_tac @{context} []")
   3.190  done
   3.191  
   3.192  
   3.193 @@ -263,15 +263,15 @@
   3.194  apply (rule_tac [3] intr_rls)
   3.195  (*case analysis on x in
   3.196      (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
   3.197 -apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac 4")
   3.198 +apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac @{context} 4")
   3.199  (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
   3.200  apply (rule_tac [5] replace_type)
   3.201  apply (rule_tac [4] replace_type)
   3.202 -apply (tactic "arith_rew_tac []")
   3.203 +apply (tactic "arith_rew_tac @{context} []")
   3.204  (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   3.205    Both follow by rewriting, (2) using quantified induction hyp*)
   3.206 -apply (tactic "intr_tac []") (*strips remaining PRODs*)
   3.207 -apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
   3.208 +apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*)
   3.209 +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *})
   3.210  apply assumption
   3.211  done
   3.212  
   3.213 @@ -293,46 +293,46 @@
   3.214  
   3.215  lemma absdiff_typing: "[| a:N;  b:N |] ==> a |-| b : N"
   3.216  apply (unfold arith_defs)
   3.217 -apply (tactic "typechk_tac []")
   3.218 +apply (tactic "typechk_tac @{context} []")
   3.219  done
   3.220  
   3.221  lemma absdiff_typingL: "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
   3.222  apply (unfold arith_defs)
   3.223 -apply (tactic "equal_tac []")
   3.224 +apply (tactic "equal_tac @{context} []")
   3.225  done
   3.226  
   3.227  lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
   3.228  apply (unfold absdiff_def)
   3.229 -apply (tactic {* arith_rew_tac [@{thm diff_self_eq_0}] *})
   3.230 +apply (tactic {* arith_rew_tac @{context} [@{thm diff_self_eq_0}] *})
   3.231  done
   3.232  
   3.233  lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
   3.234  apply (unfold absdiff_def)
   3.235 -apply (tactic "hyp_arith_rew_tac []")
   3.236 +apply (tactic "hyp_arith_rew_tac @{context} []")
   3.237  done
   3.238  
   3.239  
   3.240  lemma absdiff_succ_succ: "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
   3.241  apply (unfold absdiff_def)
   3.242 -apply (tactic "hyp_arith_rew_tac []")
   3.243 +apply (tactic "hyp_arith_rew_tac @{context} []")
   3.244  done
   3.245  
   3.246  (*Note how easy using commutative laws can be?  ...not always... *)
   3.247  lemma absdiff_commute: "[| a:N;  b:N |] ==> a |-| b = b |-| a : N"
   3.248  apply (unfold absdiff_def)
   3.249  apply (rule add_commute)
   3.250 -apply (tactic {* typechk_tac [@{thm diff_typing}] *})
   3.251 +apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *})
   3.252  done
   3.253  
   3.254  (*If a+b=0 then a=0.   Surprisingly tedious*)
   3.255  schematic_lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
   3.256  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.257  apply (rule_tac [3] replace_type)
   3.258 -apply (tactic "arith_rew_tac []")
   3.259 -apply (tactic "intr_tac []") (*strips remaining PRODs*)
   3.260 +apply (tactic "arith_rew_tac @{context} []")
   3.261 +apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*)
   3.262  apply (rule_tac [2] zero_ne_succ [THEN FE])
   3.263  apply (erule_tac [3] EqE [THEN sym_elem])
   3.264 -apply (tactic {* typechk_tac [@{thm add_typing}] *})
   3.265 +apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *})
   3.266  done
   3.267  
   3.268  (*Version of above with the premise  a+b=0.
   3.269 @@ -341,7 +341,7 @@
   3.270  apply (rule EqE)
   3.271  apply (rule add_eq0_lemma [THEN ProdE])
   3.272  apply (rule_tac [3] EqI)
   3.273 -apply (tactic "typechk_tac []")
   3.274 +apply (tactic "typechk_tac @{context} []")
   3.275  done
   3.276  
   3.277  (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
   3.278 @@ -349,12 +349,12 @@
   3.279      "[| a:N;  b:N;  a |-| b = 0 : N |] ==>
   3.280       ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
   3.281  apply (unfold absdiff_def)
   3.282 -apply (tactic "intr_tac []")
   3.283 -apply (tactic eqintr_tac)
   3.284 +apply (tactic "intr_tac @{context} []")
   3.285 +apply (tactic "eqintr_tac @{context}")
   3.286  apply (rule_tac [2] add_eq0)
   3.287  apply (rule add_eq0)
   3.288  apply (rule_tac [6] add_commute [THEN trans_elem])
   3.289 -apply (tactic {* typechk_tac [@{thm diff_typing}] *})
   3.290 +apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *})
   3.291  done
   3.292  
   3.293  (*if  a |-| b = 0  then  a = b
   3.294 @@ -362,11 +362,11 @@
   3.295  lemma absdiff_eq0: "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N"
   3.296  apply (rule EqE)
   3.297  apply (rule absdiff_eq0_lem [THEN SumE])
   3.298 -apply (tactic "TRYALL assume_tac")
   3.299 -apply (tactic eqintr_tac)
   3.300 +apply (tactic "TRYALL (assume_tac @{context})")
   3.301 +apply (tactic "eqintr_tac @{context}")
   3.302  apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
   3.303 -apply (rule_tac [3] EqE, tactic "assume_tac 3")
   3.304 -apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
   3.305 +apply (rule_tac [3] EqE, tactic "assume_tac @{context} 3")
   3.306 +apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *})
   3.307  done
   3.308  
   3.309  
   3.310 @@ -376,12 +376,12 @@
   3.311  
   3.312  lemma mod_typing: "[| a:N;  b:N |] ==> a mod b : N"
   3.313  apply (unfold mod_def)
   3.314 -apply (tactic {* typechk_tac [@{thm absdiff_typing}] *})
   3.315 +apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}] *})
   3.316  done
   3.317  
   3.318  lemma mod_typingL: "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
   3.319  apply (unfold mod_def)
   3.320 -apply (tactic {* equal_tac [@{thm absdiff_typingL}] *})
   3.321 +apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}] *})
   3.322  done
   3.323  
   3.324  
   3.325 @@ -389,13 +389,13 @@
   3.326  
   3.327  lemma modC0: "b:N ==> 0 mod b = 0 : N"
   3.328  apply (unfold mod_def)
   3.329 -apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
   3.330 +apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *})
   3.331  done
   3.332  
   3.333  lemma modC_succ:
   3.334  "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
   3.335  apply (unfold mod_def)
   3.336 -apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
   3.337 +apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *})
   3.338  done
   3.339  
   3.340  
   3.341 @@ -403,12 +403,12 @@
   3.342  
   3.343  lemma div_typing: "[| a:N;  b:N |] ==> a div b : N"
   3.344  apply (unfold div_def)
   3.345 -apply (tactic {* typechk_tac [@{thm absdiff_typing}, @{thm mod_typing}] *})
   3.346 +apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}, @{thm mod_typing}] *})
   3.347  done
   3.348  
   3.349  lemma div_typingL: "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
   3.350  apply (unfold div_def)
   3.351 -apply (tactic {* equal_tac [@{thm absdiff_typingL}, @{thm mod_typingL}] *})
   3.352 +apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}, @{thm mod_typingL}] *})
   3.353  done
   3.354  
   3.355  lemmas div_typing_rls = mod_typing div_typing absdiff_typing
   3.356 @@ -418,14 +418,14 @@
   3.357  
   3.358  lemma divC0: "b:N ==> 0 div b = 0 : N"
   3.359  apply (unfold div_def)
   3.360 -apply (tactic {* rew_tac [@{thm mod_typing}, @{thm absdiff_typing}] *})
   3.361 +apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm absdiff_typing}] *})
   3.362  done
   3.363  
   3.364  lemma divC_succ:
   3.365   "[| a:N;  b:N |] ==> succ(a) div b =
   3.366       rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
   3.367  apply (unfold div_def)
   3.368 -apply (tactic {* rew_tac [@{thm mod_typing}] *})
   3.369 +apply (tactic {* rew_tac @{context} [@{thm mod_typing}] *})
   3.370  done
   3.371  
   3.372  
   3.373 @@ -433,9 +433,9 @@
   3.374  lemma divC_succ2: "[| a:N;  b:N |] ==>
   3.375       succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
   3.376  apply (rule divC_succ [THEN trans_elem])
   3.377 -apply (tactic {* rew_tac (@{thms div_typing_rls} @ [@{thm modC_succ}]) *})
   3.378 +apply (tactic {* rew_tac @{context} (@{thms div_typing_rls} @ [@{thm modC_succ}]) *})
   3.379  apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
   3.380 -apply (tactic {* rew_tac [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *})
   3.381 +apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *})
   3.382  done
   3.383  
   3.384  (*for case analysis on whether a number is 0 or a successor*)
   3.385 @@ -444,26 +444,26 @@
   3.386  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.387  apply (rule_tac [3] PlusI_inr)
   3.388  apply (rule_tac [2] PlusI_inl)
   3.389 -apply (tactic eqintr_tac)
   3.390 -apply (tactic "equal_tac []")
   3.391 +apply (tactic "eqintr_tac @{context}")
   3.392 +apply (tactic "equal_tac @{context} []")
   3.393  done
   3.394  
   3.395  (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   3.396  lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
   3.397  apply (tactic {* NE_tac @{context} "a" 1 *})
   3.398 -apply (tactic {* arith_rew_tac (@{thms div_typing_rls} @
   3.399 +apply (tactic {* arith_rew_tac @{context} (@{thms div_typing_rls} @
   3.400    [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
   3.401  apply (rule EqE)
   3.402  (*case analysis on   succ(u mod b)|-|b  *)
   3.403  apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
   3.404  apply (erule_tac [3] SumE)
   3.405 -apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @
   3.406 +apply (tactic {* hyp_arith_rew_tac @{context} (@{thms div_typing_rls} @
   3.407    [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
   3.408  (*Replace one occurrence of  b  by succ(u mod b).  Clumsy!*)
   3.409  apply (rule add_typingL [THEN trans_elem])
   3.410  apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
   3.411  apply (rule_tac [3] refl_elem)
   3.412 -apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *})
   3.413 +apply (tactic {* hyp_arith_rew_tac @{context} @{thms div_typing_rls} *})
   3.414  done
   3.415  
   3.416  end
     4.1 --- a/src/CTT/Bool.thy	Sun Nov 09 20:49:28 2014 +0100
     4.2 +++ b/src/CTT/Bool.thy	Mon Nov 10 21:49:48 2014 +0100
     4.3 @@ -33,7 +33,7 @@
     4.4  (*formation rule*)
     4.5  lemma boolF: "Bool type"
     4.6  apply (unfold bool_defs)
     4.7 -apply (tactic "typechk_tac []")
     4.8 +apply (tactic "typechk_tac @{context} []")
     4.9  done
    4.10  
    4.11  
    4.12 @@ -41,21 +41,21 @@
    4.13  
    4.14  lemma boolI_true: "true : Bool"
    4.15  apply (unfold bool_defs)
    4.16 -apply (tactic "typechk_tac []")
    4.17 +apply (tactic "typechk_tac @{context} []")
    4.18  done
    4.19  
    4.20  lemma boolI_false: "false : Bool"
    4.21  apply (unfold bool_defs)
    4.22 -apply (tactic "typechk_tac []")
    4.23 +apply (tactic "typechk_tac @{context} []")
    4.24  done
    4.25  
    4.26  (*elimination rule: typing of cond*)
    4.27  lemma boolE: 
    4.28      "[| p:Bool;  a : C(true);  b : C(false) |] ==> cond(p,a,b) : C(p)"
    4.29  apply (unfold bool_defs)
    4.30 -apply (tactic "typechk_tac []")
    4.31 +apply (tactic "typechk_tac @{context} []")
    4.32  apply (erule_tac [!] TE)
    4.33 -apply (tactic "typechk_tac []")
    4.34 +apply (tactic "typechk_tac @{context} []")
    4.35  done
    4.36  
    4.37  lemma boolEL: 
    4.38 @@ -72,18 +72,18 @@
    4.39      "[| a : C(true);  b : C(false) |] ==> cond(true,a,b) = a : C(true)"
    4.40  apply (unfold bool_defs)
    4.41  apply (rule comp_rls)
    4.42 -apply (tactic "typechk_tac []")
    4.43 +apply (tactic "typechk_tac @{context} []")
    4.44  apply (erule_tac [!] TE)
    4.45 -apply (tactic "typechk_tac []")
    4.46 +apply (tactic "typechk_tac @{context} []")
    4.47  done
    4.48  
    4.49  lemma boolC_false: 
    4.50      "[| a : C(true);  b : C(false) |] ==> cond(false,a,b) = b : C(false)"
    4.51  apply (unfold bool_defs)
    4.52  apply (rule comp_rls)
    4.53 -apply (tactic "typechk_tac []")
    4.54 +apply (tactic "typechk_tac @{context} []")
    4.55  apply (erule_tac [!] TE)
    4.56 -apply (tactic "typechk_tac []")
    4.57 +apply (tactic "typechk_tac @{context} []")
    4.58  done
    4.59  
    4.60  end
     5.1 --- a/src/CTT/CTT.thy	Sun Nov 09 20:49:28 2014 +0100
     5.2 +++ b/src/CTT/CTT.thy	Mon Nov 10 21:49:48 2014 +0100
     5.3 @@ -336,11 +336,11 @@
     5.4  in
     5.5  
     5.6  (*Try solving a:A or a=b:A by assumption provided a is rigid!*)
     5.7 -val test_assume_tac = SUBGOAL(fn (prem,i) =>
     5.8 +fun test_assume_tac ctxt = SUBGOAL(fn (prem,i) =>
     5.9      if is_rigid_elem (Logic.strip_assums_concl prem)
    5.10 -    then  assume_tac i  else  no_tac)
    5.11 +    then  assume_tac ctxt i  else  no_tac)
    5.12  
    5.13 -fun ASSUME tf i = test_assume_tac i  ORELSE  tf i
    5.14 +fun ASSUME ctxt tf i = test_assume_tac ctxt i  ORELSE  tf i
    5.15  
    5.16  end;
    5.17  
    5.18 @@ -356,26 +356,26 @@
    5.19      @{thms elimL_rls} @ @{thms refl_elem}
    5.20  in
    5.21  
    5.22 -fun routine_tac rls prems = ASSUME (filt_resolve_tac (prems @ rls) 4);
    5.23 +fun routine_tac rls ctxt prems = ASSUME ctxt (filt_resolve_tac (prems @ rls) 4);
    5.24  
    5.25  (*Solve all subgoals "A type" using formation rules. *)
    5.26 -val form_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac @{thms form_rls} 1));
    5.27 +fun form_tac ctxt = REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac @{thms form_rls} 1));
    5.28  
    5.29  (*Type checking: solve a:A (a rigid, A flexible) by intro and elim rules. *)
    5.30 -fun typechk_tac thms =
    5.31 +fun typechk_tac ctxt thms =
    5.32    let val tac = filt_resolve_tac (thms @ @{thms form_rls} @ @{thms element_rls}) 3
    5.33 -  in  REPEAT_FIRST (ASSUME tac)  end
    5.34 +  in  REPEAT_FIRST (ASSUME ctxt tac)  end
    5.35  
    5.36  (*Solve a:A (a flexible, A rigid) by introduction rules.
    5.37    Cannot use stringtrees (filt_resolve_tac) since
    5.38    goals like ?a:SUM(A,B) have a trivial head-string *)
    5.39 -fun intr_tac thms =
    5.40 +fun intr_tac ctxt thms =
    5.41    let val tac = filt_resolve_tac(thms @ @{thms form_rls} @ @{thms intr_rls}) 1
    5.42 -  in  REPEAT_FIRST (ASSUME tac)  end
    5.43 +  in  REPEAT_FIRST (ASSUME ctxt tac)  end
    5.44  
    5.45  (*Equality proving: solve a=b:A (where a is rigid) by long rules. *)
    5.46 -fun equal_tac thms =
    5.47 -  REPEAT_FIRST (ASSUME (filt_resolve_tac (thms @ equal_rls) 3))
    5.48 +fun equal_tac ctxt thms =
    5.49 +  REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (thms @ equal_rls) 3))
    5.50  
    5.51  end
    5.52  
    5.53 @@ -408,7 +408,8 @@
    5.54  ML {*
    5.55  (*Converts each goal "e : Eq(A,a,b)" into "a=b:A" for simplification.
    5.56    Uses other intro rules to avoid changing flexible goals.*)
    5.57 -val eqintr_tac = REPEAT_FIRST (ASSUME (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
    5.58 +fun eqintr_tac ctxt =
    5.59 +  REPEAT_FIRST (ASSUME ctxt (filt_resolve_tac (@{thm EqI} :: @{thms intr_rls}) 1))
    5.60  
    5.61  (** Tactics that instantiate CTT-rules.
    5.62      Vars in the given terms will be incremented!
    5.63 @@ -426,11 +427,11 @@
    5.64  (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
    5.65  
    5.66  (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *)
    5.67 -fun add_mp_tac i =
    5.68 -    rtac @{thm subst_prodE} i  THEN  assume_tac i  THEN  assume_tac i
    5.69 +fun add_mp_tac ctxt i =
    5.70 +    rtac @{thm subst_prodE} i  THEN  assume_tac ctxt i  THEN  assume_tac ctxt i
    5.71  
    5.72  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    5.73 -fun mp_tac i = etac @{thm subst_prodE} i  THEN  assume_tac i
    5.74 +fun mp_tac ctxt i = etac @{thm subst_prodE} i  THEN  assume_tac ctxt i
    5.75  
    5.76  (*"safe" when regarded as predicate calculus rules*)
    5.77  val safe_brls = sort (make_ord lessb)
    5.78 @@ -445,18 +446,18 @@
    5.79  val (safe0_brls, safep_brls) =
    5.80      List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls
    5.81  
    5.82 -fun safestep_tac thms i =
    5.83 -    form_tac  ORELSE
    5.84 +fun safestep_tac ctxt thms i =
    5.85 +    form_tac ctxt ORELSE
    5.86      resolve_tac thms i  ORELSE
    5.87 -    biresolve_tac safe0_brls i  ORELSE  mp_tac i  ORELSE
    5.88 +    biresolve_tac safe0_brls i  ORELSE  mp_tac ctxt i  ORELSE
    5.89      DETERM (biresolve_tac safep_brls i)
    5.90  
    5.91 -fun safe_tac thms i = DEPTH_SOLVE_1 (safestep_tac thms i)
    5.92 +fun safe_tac ctxt thms i = DEPTH_SOLVE_1 (safestep_tac ctxt thms i)
    5.93  
    5.94 -fun step_tac thms = safestep_tac thms  ORELSE'  biresolve_tac unsafe_brls
    5.95 +fun step_tac ctxt thms = safestep_tac ctxt thms  ORELSE'  biresolve_tac unsafe_brls
    5.96  
    5.97  (*Fails unless it solves the goal!*)
    5.98 -fun pc_tac thms = DEPTH_SOLVE_1 o (step_tac thms)
    5.99 +fun pc_tac ctxt thms = DEPTH_SOLVE_1 o (step_tac ctxt thms)
   5.100  *}
   5.101  
   5.102  ML_file "rew.ML"
   5.103 @@ -479,7 +480,7 @@
   5.104    apply (unfold basic_defs)
   5.105    apply (rule major [THEN SumE])
   5.106    apply (rule SumC [THEN subst_eqtyparg, THEN replace_type])
   5.107 -  apply (tactic {* typechk_tac @{thms assms} *})
   5.108 +  apply (tactic {* typechk_tac @{context} @{thms assms} *})
   5.109    done
   5.110  
   5.111  end
     6.1 --- a/src/CTT/ex/Elimination.thy	Sun Nov 09 20:49:28 2014 +0100
     6.2 +++ b/src/CTT/ex/Elimination.thy	Mon Nov 10 21:49:48 2014 +0100
     6.3 @@ -15,36 +15,36 @@
     6.4  text "This finds the functions fst and snd!"
     6.5  
     6.6  schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
     6.7 -apply (tactic {* pc_tac [] 1 *})
     6.8 +apply (tactic {* pc_tac @{context} [] 1 *})
     6.9  done
    6.10  
    6.11  schematic_lemma [folded basic_defs]: "A type ==> ?a : (A*A) --> A"
    6.12 -apply (tactic {* pc_tac [] 1 *})
    6.13 +apply (tactic {* pc_tac @{context} [] 1 *})
    6.14  back
    6.15  done
    6.16  
    6.17  text "Double negation of the Excluded Middle"
    6.18  schematic_lemma "A type ==> ?a : ((A + (A-->F)) --> F) --> F"
    6.19 -apply (tactic "intr_tac []")
    6.20 +apply (tactic "intr_tac @{context} []")
    6.21  apply (rule ProdE)
    6.22  apply assumption
    6.23 -apply (tactic "pc_tac [] 1")
    6.24 +apply (tactic "pc_tac @{context} [] 1")
    6.25  done
    6.26  
    6.27  schematic_lemma "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)"
    6.28 -apply (tactic "pc_tac [] 1")
    6.29 +apply (tactic "pc_tac @{context} [] 1")
    6.30  done
    6.31  (*The sequent version (ITT) could produce an interesting alternative
    6.32    by backtracking.  No longer.*)
    6.33  
    6.34  text "Binary sums and products"
    6.35  schematic_lemma "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
    6.36 -apply (tactic "pc_tac [] 1")
    6.37 +apply (tactic "pc_tac @{context} [] 1")
    6.38  done
    6.39  
    6.40  (*A distributive law*)
    6.41  schematic_lemma "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)"
    6.42 -apply (tactic "pc_tac [] 1")
    6.43 +apply (tactic "pc_tac @{context} [] 1")
    6.44  done
    6.45  
    6.46  (*more general version, same proof*)
    6.47 @@ -53,12 +53,12 @@
    6.48      and "!!x. x:A ==> B(x) type"
    6.49      and "!!x. x:A ==> C(x) type"
    6.50    shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
    6.51 -apply (tactic {* pc_tac @{thms assms} 1 *})
    6.52 +apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
    6.53  done
    6.54  
    6.55  text "Construction of the currying functional"
    6.56  schematic_lemma "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"
    6.57 -apply (tactic "pc_tac [] 1")
    6.58 +apply (tactic "pc_tac @{context} [] 1")
    6.59  done
    6.60  
    6.61  (*more general goal with same proof*)
    6.62 @@ -68,12 +68,12 @@
    6.63      and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
    6.64    shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
    6.65                        (PROD x:A . PROD y:B(x) . C(<x,y>))"
    6.66 -apply (tactic {* pc_tac @{thms assms} 1 *})
    6.67 +apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
    6.68  done
    6.69  
    6.70  text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
    6.71  schematic_lemma "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"
    6.72 -apply (tactic "pc_tac [] 1")
    6.73 +apply (tactic "pc_tac @{context} [] 1")
    6.74  done
    6.75  
    6.76  (*more general goal with same proof*)
    6.77 @@ -83,12 +83,12 @@
    6.78      and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
    6.79    shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
    6.80          --> (PROD z : (SUM x:A . B(x)) . C(z))"
    6.81 -apply (tactic {* pc_tac @{thms assms} 1 *})
    6.82 +apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
    6.83  done
    6.84  
    6.85  text "Function application"
    6.86  schematic_lemma "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B"
    6.87 -apply (tactic "pc_tac [] 1")
    6.88 +apply (tactic "pc_tac @{context} [] 1")
    6.89  done
    6.90  
    6.91  text "Basic test of quantifier reasoning"
    6.92 @@ -99,7 +99,7 @@
    6.93    shows
    6.94      "?a :     (SUM y:B . PROD x:A . C(x,y))
    6.95            --> (PROD x:A . SUM y:B . C(x,y))"
    6.96 -apply (tactic {* pc_tac @{thms assms} 1 *})
    6.97 +apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
    6.98  done
    6.99  
   6.100  text "Martin-Lof (1984) pages 36-7: the combinator S"
   6.101 @@ -109,7 +109,7 @@
   6.102      and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
   6.103    shows "?a :    (PROD x:A. PROD y:B(x). C(x,y))
   6.104               --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
   6.105 -apply (tactic {* pc_tac @{thms assms} 1 *})
   6.106 +apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
   6.107  done
   6.108  
   6.109  text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
   6.110 @@ -119,13 +119,13 @@
   6.111      and "!!z. z: A+B ==> C(z) type"
   6.112    shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
   6.113            --> (PROD z: A+B. C(z))"
   6.114 -apply (tactic {* pc_tac @{thms assms} 1 *})
   6.115 +apply (tactic {* pc_tac @{context} @{thms assms} 1 *})
   6.116  done
   6.117  
   6.118  (*towards AXIOM OF CHOICE*)
   6.119  schematic_lemma [folded basic_defs]:
   6.120    "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
   6.121 -apply (tactic "pc_tac [] 1")
   6.122 +apply (tactic "pc_tac @{context} [] 1")
   6.123  done
   6.124  
   6.125  
   6.126 @@ -137,15 +137,15 @@
   6.127      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
   6.128    shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
   6.129                           (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
   6.130 -apply (tactic {* intr_tac @{thms assms} *})
   6.131 -apply (tactic "add_mp_tac 2")
   6.132 -apply (tactic "add_mp_tac 1")
   6.133 +apply (tactic {* intr_tac @{context} @{thms assms} *})
   6.134 +apply (tactic "add_mp_tac @{context} 2")
   6.135 +apply (tactic "add_mp_tac @{context} 1")
   6.136  apply (erule SumE_fst)
   6.137  apply (rule replace_type)
   6.138  apply (rule subst_eqtyparg)
   6.139  apply (rule comp_rls)
   6.140  apply (rule_tac [4] SumE_snd)
   6.141 -apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms assms}) *})
   6.142 +apply (tactic {* typechk_tac @{context} (@{thm SumE_fst} :: @{thms assms}) *})
   6.143  done
   6.144  
   6.145  text "Axiom of choice.  Proof without fst, snd.  Harder still!"
   6.146 @@ -155,19 +155,19 @@
   6.147      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
   6.148    shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
   6.149                           (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
   6.150 -apply (tactic {* intr_tac @{thms assms} *})
   6.151 +apply (tactic {* intr_tac @{context} @{thms assms} *})
   6.152  (*Must not use add_mp_tac as subst_prodE hides the construction.*)
   6.153  apply (rule ProdE [THEN SumE], assumption)
   6.154 -apply (tactic "TRYALL assume_tac")
   6.155 +apply (tactic "TRYALL (assume_tac @{context})")
   6.156  apply (rule replace_type)
   6.157  apply (rule subst_eqtyparg)
   6.158  apply (rule comp_rls)
   6.159  apply (erule_tac [4] ProdE [THEN SumE])
   6.160 -apply (tactic {* typechk_tac @{thms assms} *})
   6.161 +apply (tactic {* typechk_tac @{context} @{thms assms} *})
   6.162  apply (rule replace_type)
   6.163  apply (rule subst_eqtyparg)
   6.164  apply (rule comp_rls)
   6.165 -apply (tactic {* typechk_tac @{thms assms} *})
   6.166 +apply (tactic {* typechk_tac @{context} @{thms assms} *})
   6.167  apply assumption
   6.168  done
   6.169  
   6.170 @@ -183,11 +183,11 @@
   6.171  apply (tactic {* biresolve_tac safe_brls 2 *})
   6.172  (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
   6.173  apply (rule_tac [2] a = "y" in ProdE)
   6.174 -apply (tactic {* typechk_tac @{thms assms} *})
   6.175 +apply (tactic {* typechk_tac @{context} @{thms assms} *})
   6.176  apply (rule SumE, assumption)
   6.177 -apply (tactic "intr_tac []")
   6.178 -apply (tactic "TRYALL assume_tac")
   6.179 -apply (tactic {* typechk_tac @{thms assms} *})
   6.180 +apply (tactic "intr_tac @{context} []")
   6.181 +apply (tactic "TRYALL (assume_tac @{context})")
   6.182 +apply (tactic {* typechk_tac @{context} @{thms assms} *})
   6.183  done
   6.184  
   6.185  end
     7.1 --- a/src/CTT/ex/Equality.thy	Sun Nov 09 20:49:28 2014 +0100
     7.2 +++ b/src/CTT/ex/Equality.thy	Mon Nov 10 21:49:48 2014 +0100
     7.3 @@ -12,27 +12,27 @@
     7.4  lemma split_eq: "p : Sum(A,B) ==> split(p,pair) = p : Sum(A,B)"
     7.5  apply (rule EqE)
     7.6  apply (rule elim_rls, assumption)
     7.7 -apply (tactic "rew_tac []")
     7.8 +apply (tactic "rew_tac @{context} []")
     7.9  done
    7.10  
    7.11  lemma when_eq: "[| A type;  B type;  p : A+B |] ==> when(p,inl,inr) = p : A + B"
    7.12  apply (rule EqE)
    7.13  apply (rule elim_rls, assumption)
    7.14 -apply (tactic "rew_tac []")
    7.15 +apply (tactic "rew_tac @{context} []")
    7.16  done
    7.17  
    7.18  (*in the "rec" formulation of addition, 0+n=n *)
    7.19  lemma "p:N ==> rec(p,0, %y z. succ(y)) = p : N"
    7.20  apply (rule EqE)
    7.21  apply (rule elim_rls, assumption)
    7.22 -apply (tactic "rew_tac []")
    7.23 +apply (tactic "rew_tac @{context} []")
    7.24  done
    7.25  
    7.26  (*the harder version, n+0=n: recursive, uses induction hypothesis*)
    7.27  lemma "p:N ==> rec(p,0, %y z. succ(z)) = p : N"
    7.28  apply (rule EqE)
    7.29  apply (rule elim_rls, assumption)
    7.30 -apply (tactic "hyp_rew_tac []")
    7.31 +apply (tactic "hyp_rew_tac @{context} []")
    7.32  done
    7.33  
    7.34  (*Associativity of addition*)
    7.35 @@ -40,19 +40,19 @@
    7.36        ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) =
    7.37            rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N"
    7.38  apply (tactic {* NE_tac @{context} "a" 1 *})
    7.39 -apply (tactic "hyp_rew_tac []")
    7.40 +apply (tactic "hyp_rew_tac @{context} []")
    7.41  done
    7.42  
    7.43  (*Martin-Lof (1984) page 62: pairing is surjective*)
    7.44  lemma "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)"
    7.45  apply (rule EqE)
    7.46  apply (rule elim_rls, assumption)
    7.47 -apply (tactic {* DEPTH_SOLVE_1 (rew_tac []) *}) (*!!!!!!!*)
    7.48 +apply (tactic {* DEPTH_SOLVE_1 (rew_tac @{context} []) *}) (*!!!!!!!*)
    7.49  done
    7.50  
    7.51  lemma "[| a : A;  b : B |] ==>
    7.52       (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
    7.53 -apply (tactic "rew_tac []")
    7.54 +apply (tactic "rew_tac @{context} []")
    7.55  done
    7.56  
    7.57  (*a contrived, complicated simplication, requires sum-elimination also*)
    7.58 @@ -61,9 +61,9 @@
    7.59  apply (rule reduction_rls)
    7.60  apply (rule_tac [3] intrL_rls)
    7.61  apply (rule_tac [4] EqE)
    7.62 -apply (rule_tac [4] SumE, tactic "assume_tac 4")
    7.63 +apply (rule_tac [4] SumE, tactic "assume_tac @{context} 4")
    7.64  (*order of unifiers is essential here*)
    7.65 -apply (tactic "rew_tac []")
    7.66 +apply (tactic "rew_tac @{context} []")
    7.67  done
    7.68  
    7.69  end
     8.1 --- a/src/CTT/ex/Synthesis.thy	Sun Nov 09 20:49:28 2014 +0100
     8.2 +++ b/src/CTT/ex/Synthesis.thy	Mon Nov 10 21:49:48 2014 +0100
     8.3 @@ -12,21 +12,21 @@
     8.4  text "discovery of predecessor function"
     8.5  schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)
     8.6                    *  (PROD n:N. Eq(N, pred ` succ(n), n))"
     8.7 -apply (tactic "intr_tac []")
     8.8 -apply (tactic eqintr_tac)
     8.9 +apply (tactic "intr_tac @{context} []")
    8.10 +apply (tactic "eqintr_tac @{context}")
    8.11  apply (rule_tac [3] reduction_rls)
    8.12  apply (rule_tac [5] comp_rls)
    8.13 -apply (tactic "rew_tac []")
    8.14 +apply (tactic "rew_tac @{context} []")
    8.15  done
    8.16  
    8.17  text "the function fst as an element of a function type"
    8.18  schematic_lemma [folded basic_defs]:
    8.19    "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
    8.20 -apply (tactic "intr_tac []")
    8.21 -apply (tactic eqintr_tac)
    8.22 +apply (tactic "intr_tac @{context} []")
    8.23 +apply (tactic "eqintr_tac @{context}")
    8.24  apply (rule_tac [2] reduction_rls)
    8.25  apply (rule_tac [4] comp_rls)
    8.26 -apply (tactic "typechk_tac []")
    8.27 +apply (tactic "typechk_tac @{context} []")
    8.28  txt "now put in A everywhere"
    8.29  apply assumption+
    8.30  done
    8.31 @@ -36,10 +36,10 @@
    8.32    See following example.*)
    8.33  schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
    8.34                     * Eq(?A, ?b(inr(i)), <succ(0), i>)"
    8.35 -apply (tactic "intr_tac []")
    8.36 -apply (tactic eqintr_tac)
    8.37 +apply (tactic "intr_tac @{context} []")
    8.38 +apply (tactic "eqintr_tac @{context}")
    8.39  apply (rule comp_rls)
    8.40 -apply (tactic "rew_tac []")
    8.41 +apply (tactic "rew_tac @{context} []")
    8.42  done
    8.43  
    8.44  (*Here we allow the type to depend on i.
    8.45 @@ -55,13 +55,13 @@
    8.46  schematic_lemma [folded basic_defs]:
    8.47    "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
    8.48                             *  Eq(?A, ?b(inr(<i,j>)), j)"
    8.49 -apply (tactic "intr_tac []")
    8.50 -apply (tactic eqintr_tac)
    8.51 +apply (tactic "intr_tac @{context} []")
    8.52 +apply (tactic "eqintr_tac @{context}")
    8.53  apply (rule PlusC_inl [THEN trans_elem])
    8.54  apply (rule_tac [4] comp_rls)
    8.55  apply (rule_tac [7] reduction_rls)
    8.56  apply (rule_tac [10] comp_rls)
    8.57 -apply (tactic "typechk_tac []")
    8.58 +apply (tactic "typechk_tac @{context} []")
    8.59  done
    8.60  
    8.61  (*similar but allows the type to depend on i and j*)
    8.62 @@ -79,10 +79,10 @@
    8.63  schematic_lemma [folded arith_defs]:
    8.64    "?c : PROD n:N. Eq(N, ?f(0,n), n)
    8.65                    *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
    8.66 -apply (tactic "intr_tac []")
    8.67 -apply (tactic eqintr_tac)
    8.68 +apply (tactic "intr_tac @{context} []")
    8.69 +apply (tactic "eqintr_tac @{context}")
    8.70  apply (rule comp_rls)
    8.71 -apply (tactic "rew_tac []")
    8.72 +apply (tactic "rew_tac @{context} []")
    8.73  done
    8.74  
    8.75  text "The addition function -- using explicit lambdas"
    8.76 @@ -90,15 +90,15 @@
    8.77    "?c : SUM plus : ?A .
    8.78           PROD x:N. Eq(N, plus`0`x, x)
    8.79                  *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
    8.80 -apply (tactic "intr_tac []")
    8.81 -apply (tactic eqintr_tac)
    8.82 +apply (tactic "intr_tac @{context} []")
    8.83 +apply (tactic "eqintr_tac @{context}")
    8.84  apply (tactic "resolve_tac [TSimp.split_eqn] 3")
    8.85 -apply (tactic "SELECT_GOAL (rew_tac []) 4")
    8.86 +apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
    8.87  apply (tactic "resolve_tac [TSimp.split_eqn] 3")
    8.88 -apply (tactic "SELECT_GOAL (rew_tac []) 4")
    8.89 +apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
    8.90  apply (rule_tac [3] p = "y" in NC_succ)
    8.91    (**  by (resolve_tac comp_rls 3);  caused excessive branching  **)
    8.92 -apply (tactic "rew_tac []")
    8.93 +apply (tactic "rew_tac @{context} []")
    8.94  done
    8.95  
    8.96  end
     9.1 --- a/src/CTT/ex/Typechecking.thy	Sun Nov 09 20:49:28 2014 +0100
     9.2 +++ b/src/CTT/ex/Typechecking.thy	Mon Nov 10 21:49:48 2014 +0100
     9.3 @@ -34,34 +34,34 @@
     9.4  subsection {* Multi-step proofs: Type inference *}
     9.5  
     9.6  lemma "PROD w:N. N + N type"
     9.7 -apply (tactic form_tac)
     9.8 +apply (tactic "form_tac @{context}")
     9.9  done
    9.10  
    9.11  schematic_lemma "<0, succ(0)> : ?A"
    9.12 -apply (tactic "intr_tac []")
    9.13 +apply (tactic "intr_tac @{context} []")
    9.14  done
    9.15  
    9.16  schematic_lemma "PROD w:N . Eq(?A,w,w) type"
    9.17 -apply (tactic "typechk_tac []")
    9.18 +apply (tactic "typechk_tac @{context} []")
    9.19  done
    9.20  
    9.21  schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type"
    9.22 -apply (tactic "typechk_tac []")
    9.23 +apply (tactic "typechk_tac @{context} []")
    9.24  done
    9.25  
    9.26  text "typechecking an application of fst"
    9.27  schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A"
    9.28 -apply (tactic "typechk_tac []")
    9.29 +apply (tactic "typechk_tac @{context} []")
    9.30  done
    9.31  
    9.32  text "typechecking the predecessor function"
    9.33  schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A"
    9.34 -apply (tactic "typechk_tac []")
    9.35 +apply (tactic "typechk_tac @{context} []")
    9.36  done
    9.37  
    9.38  text "typechecking the addition function"
    9.39  schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A"
    9.40 -apply (tactic "typechk_tac []")
    9.41 +apply (tactic "typechk_tac @{context} []")
    9.42  done
    9.43  
    9.44  (*Proofs involving arbitrary types.
    9.45 @@ -69,18 +69,18 @@
    9.46  ML {* val N_tac = TRYALL (rtac @{thm NF}) *}
    9.47  
    9.48  schematic_lemma "lam w. <w,w> : ?A"
    9.49 -apply (tactic "typechk_tac []")
    9.50 +apply (tactic "typechk_tac @{context} []")
    9.51  apply (tactic N_tac)
    9.52  done
    9.53  
    9.54  schematic_lemma "lam x. lam y. x : ?A"
    9.55 -apply (tactic "typechk_tac []")
    9.56 +apply (tactic "typechk_tac @{context} []")
    9.57  apply (tactic N_tac)
    9.58  done
    9.59  
    9.60  text "typechecking fst (as a function object)"
    9.61  schematic_lemma "lam i. split(i, %j k. j) : ?A"
    9.62 -apply (tactic "typechk_tac []")
    9.63 +apply (tactic "typechk_tac @{context} []")
    9.64  apply (tactic N_tac)
    9.65  done
    9.66  
    10.1 --- a/src/CTT/rew.ML	Sun Nov 09 20:49:28 2014 +0100
    10.2 +++ b/src/CTT/rew.ML	Mon Nov 10 21:49:48 2014 +0100
    10.3 @@ -23,7 +23,7 @@
    10.4    val trans_red         = @{thm trans_red}
    10.5    val red_if_equal      = @{thm red_if_equal}
    10.6    val default_rls       = @{thms comp_rls}
    10.7 -  val routine_tac       = routine_tac (@{thms routine_rls})
    10.8 +  val routine_tac       = routine_tac @{thms routine_rls}
    10.9    end;
   10.10  
   10.11  structure TSimp = TSimpFun (TSimp_data);
   10.12 @@ -31,12 +31,12 @@
   10.13  val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls};
   10.14  
   10.15  (*Make a rewriting tactic from a normalization tactic*)
   10.16 -fun make_rew_tac ntac =
   10.17 -    TRY eqintr_tac  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  
   10.18 +fun make_rew_tac ctxt ntac =
   10.19 +    TRY (eqintr_tac ctxt)  THEN  TRYALL (resolve_tac [TSimp.split_eqn])  THEN  
   10.20      ntac;
   10.21  
   10.22 -fun rew_tac thms = make_rew_tac
   10.23 -    (TSimp.norm_tac(standard_congr_rls, thms));
   10.24 +fun rew_tac ctxt thms = make_rew_tac ctxt
   10.25 +    (TSimp.norm_tac ctxt (standard_congr_rls, thms));
   10.26  
   10.27 -fun hyp_rew_tac thms = make_rew_tac
   10.28 -    (TSimp.cond_norm_tac(prove_cond_tac, standard_congr_rls, thms));
   10.29 +fun hyp_rew_tac ctxt thms = make_rew_tac ctxt
   10.30 +    (TSimp.cond_norm_tac ctxt (prove_cond_tac, standard_congr_rls, thms));
    11.1 --- a/src/Doc/Implementation/Tactic.thy	Sun Nov 09 20:49:28 2014 +0100
    11.2 +++ b/src/Doc/Implementation/Tactic.thy	Mon Nov 10 21:49:48 2014 +0100
    11.3 @@ -282,7 +282,7 @@
    11.4    @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
    11.5    @{index_ML forward_tac: "thm list -> int -> tactic"} \\
    11.6    @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
    11.7 -  @{index_ML assume_tac: "int -> tactic"} \\
    11.8 +  @{index_ML assume_tac: "Proof.context -> int -> tactic"} \\
    11.9    @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
   11.10    @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
   11.11    @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
   11.12 @@ -324,7 +324,7 @@
   11.13    elimination rules, which is useful to organize the search process
   11.14    systematically in proof tools.
   11.15  
   11.16 -  \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
   11.17 +  \item @{ML assume_tac}~@{text "ctxt i"} attempts to solve subgoal @{text i}
   11.18    by assumption (modulo higher-order unification).
   11.19  
   11.20    \item @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
    12.1 --- a/src/Doc/Isar_Ref/Generic.thy	Sun Nov 09 20:49:28 2014 +0100
    12.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Mon Nov 10 21:49:48 2014 +0100
    12.3 @@ -1053,7 +1053,7 @@
    12.4  
    12.5  ML \<open>
    12.6    fun subgoaler_tac ctxt =
    12.7 -    assume_tac ORELSE'
    12.8 +    assume_tac ctxt ORELSE'
    12.9      resolve_tac (Simplifier.prems_of ctxt) ORELSE'
   12.10      asm_simp_tac ctxt
   12.11  \<close>
    13.1 --- a/src/Doc/Tutorial/Protocol/Event.thy	Sun Nov 09 20:49:28 2014 +0100
    13.2 +++ b/src/Doc/Tutorial/Protocol/Event.thy	Mon Nov 10 21:49:48 2014 +0100
    13.3 @@ -260,10 +260,10 @@
    13.4  
    13.5  ML
    13.6  {*
    13.7 -val analz_mono_contra_tac = 
    13.8 +fun analz_mono_contra_tac ctxt =
    13.9    rtac @{thm analz_impI} THEN' 
   13.10    REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
   13.11 -  THEN' mp_tac
   13.12 +  THEN' mp_tac ctxt
   13.13  *}
   13.14  
   13.15  lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
   13.16 @@ -285,7 +285,7 @@
   13.17      intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
   13.18  
   13.19  method_setup analz_mono_contra = {*
   13.20 -    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
   13.21 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
   13.22      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   13.23  
   13.24  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
   13.25 @@ -330,7 +330,7 @@
   13.26  val knows_Spy_subset_knows_Spy_Gets = @{thm knows_Spy_subset_knows_Spy_Gets};
   13.27  
   13.28  
   13.29 -val synth_analz_mono_contra_tac = 
   13.30 +fun synth_analz_mono_contra_tac ctxt = 
   13.31    rtac @{thm syan_impI} THEN'
   13.32    REPEAT1 o 
   13.33      (dresolve_tac 
   13.34 @@ -338,11 +338,11 @@
   13.35        @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
   13.36        @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
   13.37    THEN'
   13.38 -  mp_tac
   13.39 +  mp_tac ctxt
   13.40  *}
   13.41  
   13.42  method_setup synth_analz_mono_contra = {*
   13.43 -    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
   13.44 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *}
   13.45      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
   13.46  (*>*)
   13.47  
    14.1 --- a/src/FOL/IFOL.thy	Sun Nov 09 20:49:28 2014 +0100
    14.2 +++ b/src/FOL/IFOL.thy	Mon Nov 10 21:49:48 2014 +0100
    14.3 @@ -208,7 +208,7 @@
    14.4  
    14.5  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    14.6  ML {*
    14.7 -  fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  assume_tac i
    14.8 +  fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  atac i
    14.9    fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  eq_assume_tac i
   14.10  *}
   14.11  
    15.1 --- a/src/FOL/intprover.ML	Sun Nov 09 20:49:28 2014 +0100
    15.2 +++ b/src/FOL/intprover.ML	Mon Nov 10 21:49:48 2014 +0100
    15.3 @@ -20,7 +20,7 @@
    15.4    val best_tac: Proof.context -> int -> tactic
    15.5    val best_dup_tac: Proof.context -> int -> tactic
    15.6    val fast_tac: Proof.context -> int -> tactic
    15.7 -  val inst_step_tac: int -> tactic
    15.8 +  val inst_step_tac: Proof.context -> int -> tactic
    15.9    val safe_step_tac: Proof.context -> int -> tactic
   15.10    val safe_brls: (bool * thm) list
   15.11    val safe_tac: Proof.context -> tactic
   15.12 @@ -74,14 +74,14 @@
   15.13  fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
   15.14  
   15.15  (*These steps could instantiate variables and are therefore unsafe.*)
   15.16 -val inst_step_tac =
   15.17 -  assume_tac APPEND' mp_tac APPEND' 
   15.18 +fun inst_step_tac ctxt =
   15.19 +  assume_tac ctxt APPEND' mp_tac APPEND' 
   15.20    biresolve_tac (safe0_brls @ safep_brls);
   15.21  
   15.22  (*One safe or unsafe step. *)
   15.23 -fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_brls i];
   15.24 +fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_brls i];
   15.25  
   15.26 -fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_brls i];
   15.27 +fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_dup_brls i];
   15.28  
   15.29  (*Dumb but fast*)
   15.30  fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
    16.1 --- a/src/FOL/simpdata.ML	Sun Nov 09 20:49:28 2014 +0100
    16.2 +++ b/src/FOL/simpdata.ML	Mon Nov 10 21:49:48 2014 +0100
    16.3 @@ -108,7 +108,7 @@
    16.4  
    16.5  fun unsafe_solver ctxt =
    16.6    FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt),
    16.7 -    assume_tac,
    16.8 +    assume_tac ctxt,
    16.9      eresolve_tac @{thms FalseE}];
   16.10  
   16.11  (*No premature instantiation of variables during simplification*)
    17.1 --- a/src/FOLP/IFOLP.thy	Sun Nov 09 20:49:28 2014 +0100
    17.2 +++ b/src/FOLP/IFOLP.thy	Mon Nov 10 21:49:48 2014 +0100
    17.3 @@ -252,7 +252,7 @@
    17.4  local
    17.5    fun discard_proof (Const (@{const_name Proof}, _) $ P $ _) = P;
    17.6  in
    17.7 -val uniq_assume_tac =
    17.8 +fun uniq_assume_tac ctxt =
    17.9    SUBGOAL
   17.10      (fn (prem,i) =>
   17.11        let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
   17.12 @@ -260,7 +260,7 @@
   17.13        in
   17.14            if exists (fn hyp => hyp aconv concl) hyps
   17.15            then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
   17.16 -                   [_] => assume_tac i
   17.17 +                   [_] => assume_tac ctxt i
   17.18                   |  _  => no_tac
   17.19            else no_tac
   17.20        end);
   17.21 @@ -272,12 +272,14 @@
   17.22  
   17.23  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   17.24  ML {*
   17.25 -  fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac i
   17.26 +  fun mp_tac ctxt i =
   17.27 +    eresolve_tac [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac ctxt i
   17.28  *}
   17.29  
   17.30  (*Like mp_tac but instantiates no variables*)
   17.31  ML {*
   17.32 -  fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  uniq_assume_tac i
   17.33 +  fun int_uniq_mp_tac ctxt i =
   17.34 +    eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  uniq_assume_tac ctxt i
   17.35  *}
   17.36  
   17.37  
   17.38 @@ -374,7 +376,7 @@
   17.39  
   17.40  schematic_lemma disj_cong:
   17.41    "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
   17.42 -  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
   17.43 +  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
   17.44    done
   17.45  
   17.46  schematic_lemma imp_cong:
   17.47 @@ -382,31 +384,31 @@
   17.48      and "!!x. x:P' ==> q(x):Q <-> Q'"
   17.49    shows "?p:(P-->Q) <-> (P'-->Q')"
   17.50    apply (insert assms(1))
   17.51 -  apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} |
   17.52 +  apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac @{context} 1 *} |
   17.53      tactic {* iff_tac @{thms assms} 1 *})+
   17.54    done
   17.55  
   17.56  schematic_lemma iff_cong:
   17.57    "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
   17.58 -  apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
   17.59 +  apply (erule iffE | assumption | rule iffI | tactic {* mp_tac @{context} 1 *})+
   17.60    done
   17.61  
   17.62  schematic_lemma not_cong:
   17.63    "p:P <-> P' ==> ?p:~P <-> ~P'"
   17.64 -  apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
   17.65 +  apply (assumption | rule iffI notI | tactic {* mp_tac @{context} 1 *} | erule iffE notE)+
   17.66    done
   17.67  
   17.68  schematic_lemma all_cong:
   17.69    assumes "!!x. f(x):P(x) <-> Q(x)"
   17.70    shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
   17.71 -  apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
   17.72 +  apply (assumption | rule iffI allI | tactic {* mp_tac @{context} 1 *} | erule allE |
   17.73      tactic {* iff_tac @{thms assms} 1 *})+
   17.74    done
   17.75  
   17.76  schematic_lemma ex_cong:
   17.77    assumes "!!x. f(x):P(x) <-> Q(x)"
   17.78    shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
   17.79 -  apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
   17.80 +  apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac @{context} 1 *} |
   17.81      tactic {* iff_tac @{thms assms} 1 *})+
   17.82    done
   17.83  
   17.84 @@ -636,7 +638,7 @@
   17.85    "?p6 : P & ~P <-> False"
   17.86    "?p7 : ~P & P <-> False"
   17.87    "?p8 : (P & Q) & R <-> P & (Q & R)"
   17.88 -  apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
   17.89 +  apply (tactic {* fn st => IntPr.fast_tac @{context} 1 st *})+
   17.90    done
   17.91  
   17.92  schematic_lemma disj_rews:
   17.93 @@ -646,13 +648,13 @@
   17.94    "?p4 : False | P <-> P"
   17.95    "?p5 : P | P <-> P"
   17.96    "?p6 : (P | Q) | R <-> P | (Q | R)"
   17.97 -  apply (tactic {* IntPr.fast_tac 1 *})+
   17.98 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
   17.99    done
  17.100  
  17.101  schematic_lemma not_rews:
  17.102    "?p1 : ~ False <-> True"
  17.103    "?p2 : ~ True <-> False"
  17.104 -  apply (tactic {* IntPr.fast_tac 1 *})+
  17.105 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
  17.106    done
  17.107  
  17.108  schematic_lemma imp_rews:
  17.109 @@ -662,7 +664,7 @@
  17.110    "?p4 : (True --> P) <-> P"
  17.111    "?p5 : (P --> P) <-> True"
  17.112    "?p6 : (P --> ~P) <-> ~P"
  17.113 -  apply (tactic {* IntPr.fast_tac 1 *})+
  17.114 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
  17.115    done
  17.116  
  17.117  schematic_lemma iff_rews:
  17.118 @@ -671,13 +673,13 @@
  17.119    "?p3 : (P <-> P) <-> True"
  17.120    "?p4 : (False <-> P) <-> ~P"
  17.121    "?p5 : (P <-> False) <-> ~P"
  17.122 -  apply (tactic {* IntPr.fast_tac 1 *})+
  17.123 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
  17.124    done
  17.125  
  17.126  schematic_lemma quant_rews:
  17.127    "?p1 : (ALL x. P) <-> P"
  17.128    "?p2 : (EX x. P) <-> P"
  17.129 -  apply (tactic {* IntPr.fast_tac 1 *})+
  17.130 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
  17.131    done
  17.132  
  17.133  (*These are NOT supplied by default!*)
  17.134 @@ -686,7 +688,7 @@
  17.135    "?p2 : P & (Q | R) <-> P&Q | P&R"
  17.136    "?p3 : (Q | R) & P <-> Q&P | R&P"
  17.137    "?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)"
  17.138 -  apply (tactic {* IntPr.fast_tac 1 *})+
  17.139 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
  17.140    done
  17.141  
  17.142  schematic_lemma distrib_rews2:
  17.143 @@ -694,17 +696,17 @@
  17.144    "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
  17.145    "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
  17.146    "?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"
  17.147 -  apply (tactic {* IntPr.fast_tac 1 *})+
  17.148 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})+
  17.149    done
  17.150  
  17.151  lemmas distrib_rews = distrib_rews1 distrib_rews2
  17.152  
  17.153  schematic_lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
  17.154 -  apply (tactic {* IntPr.fast_tac 1 *})
  17.155 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})
  17.156    done
  17.157  
  17.158  schematic_lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
  17.159 -  apply (tactic {* IntPr.fast_tac 1 *})
  17.160 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})
  17.161    done
  17.162  
  17.163  end
    18.1 --- a/src/FOLP/classical.ML	Sun Nov 09 20:49:28 2014 +0100
    18.2 +++ b/src/FOLP/classical.ML	Mon Nov 10 21:49:48 2014 +0100
    18.3 @@ -45,17 +45,17 @@
    18.4         safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
    18.5         haz_brls: (bool*thm)list}
    18.6    val best_tac : Proof.context -> claset -> int -> tactic
    18.7 -  val contr_tac : int -> tactic
    18.8 +  val contr_tac : Proof.context -> int -> tactic
    18.9    val fast_tac : Proof.context -> claset -> int -> tactic
   18.10 -  val inst_step_tac : int -> tactic
   18.11 +  val inst_step_tac : Proof.context -> int -> tactic
   18.12    val joinrules : thm list * thm list -> (bool * thm) list
   18.13 -  val mp_tac: int -> tactic
   18.14 +  val mp_tac: Proof.context -> int -> tactic
   18.15    val safe_tac : Proof.context -> claset -> tactic
   18.16    val safe_step_tac : Proof.context -> claset -> int -> tactic
   18.17    val slow_step_tac : Proof.context -> claset -> int -> tactic
   18.18    val step_tac : Proof.context -> claset -> int -> tactic
   18.19    val swapify : thm list -> thm list
   18.20 -  val swap_res_tac : thm list -> int -> tactic
   18.21 +  val swap_res_tac : Proof.context -> thm list -> int -> tactic
   18.22    val uniq_mp_tac: Proof.context -> int -> tactic
   18.23    end;
   18.24  
   18.25 @@ -70,22 +70,22 @@
   18.26  val imp_elim = make_elim mp;
   18.27  
   18.28  (*Solve goal that assumes both P and ~P. *)
   18.29 -val contr_tac = etac not_elim THEN'  assume_tac;
   18.30 +fun contr_tac ctxt = etac not_elim THEN'  assume_tac ctxt;
   18.31  
   18.32  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   18.33 -fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
   18.34 +fun mp_tac ctxt i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac ctxt i;
   18.35  
   18.36  (*Like mp_tac but instantiates no variables*)
   18.37 -fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
   18.38 +fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac ctxt i;
   18.39  
   18.40  (*Creates rules to eliminate ~A, from rules to introduce A*)
   18.41  fun swapify intrs = intrs RLN (2, [swap]);
   18.42  
   18.43  (*Uses introduction rules in the normal way, or on negated assumptions,
   18.44    trying rules in order. *)
   18.45 -fun swap_res_tac rls = 
   18.46 +fun swap_res_tac ctxt rls = 
   18.47      let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap))
   18.48 -    in  assume_tac ORELSE' contr_tac ORELSE' FIRST' (map tacf rls)
   18.49 +    in  assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls)
   18.50      end;
   18.51  
   18.52  
   18.53 @@ -149,7 +149,7 @@
   18.54  
   18.55  (*Attack subgoals using safe inferences*)
   18.56  fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 
   18.57 -  FIRST' [uniq_assume_tac,
   18.58 +  FIRST' [uniq_assume_tac ctxt,
   18.59            uniq_mp_tac ctxt,
   18.60            biresolve_tac safe0_brls,
   18.61            FIRST' hyp_subst_tacs,
   18.62 @@ -159,12 +159,12 @@
   18.63  fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
   18.64  
   18.65  (*These steps could instantiate variables and are therefore unsafe.*)
   18.66 -val inst_step_tac = assume_tac APPEND' contr_tac;
   18.67 +fun inst_step_tac ctxt = assume_tac ctxt APPEND' contr_tac ctxt;
   18.68  
   18.69  (*Single step for the prover.  FAILS unless it makes progress. *)
   18.70  fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 
   18.71    FIRST [safe_tac ctxt cs,
   18.72 -         inst_step_tac i,
   18.73 +         inst_step_tac ctxt i,
   18.74           biresolve_tac haz_brls i];
   18.75  
   18.76  (*** The following tactics all fail unless they solve one goal ***)
   18.77 @@ -179,7 +179,7 @@
   18.78  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   18.79    allows backtracking from "safe" rules to "unsafe" rules here.*)
   18.80  fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 
   18.81 -    safe_tac ctxt cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
   18.82 +    safe_tac ctxt cs ORELSE (assume_tac ctxt i APPEND biresolve_tac haz_brls i);
   18.83  
   18.84  end; 
   18.85  end;
    19.1 --- a/src/FOLP/ex/Intuitionistic.thy	Sun Nov 09 20:49:28 2014 +0100
    19.2 +++ b/src/FOLP/ex/Intuitionistic.thy	Mon Nov 10 21:49:48 2014 +0100
    19.3 @@ -31,39 +31,39 @@
    19.4  begin
    19.5  
    19.6  schematic_lemma "?p : ~~(P&Q) <-> ~~P & ~~Q"
    19.7 -  by (tactic {* IntPr.fast_tac 1 *})
    19.8 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
    19.9  
   19.10  schematic_lemma "?p : ~~~P <-> ~P"
   19.11 -  by (tactic {* IntPr.fast_tac 1 *})
   19.12 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.13  
   19.14  schematic_lemma "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
   19.15 -  by (tactic {* IntPr.fast_tac 1 *})
   19.16 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.17  
   19.18  schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
   19.19 -  by (tactic {* IntPr.fast_tac 1 *})
   19.20 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.21  
   19.22  
   19.23  subsection {* Lemmas for the propositional double-negation translation *}
   19.24  
   19.25  schematic_lemma "?p : P --> ~~P"
   19.26 -  by (tactic {* IntPr.fast_tac 1 *})
   19.27 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.28  
   19.29  schematic_lemma "?p : ~~(~~P --> P)"
   19.30 -  by (tactic {* IntPr.fast_tac 1 *})
   19.31 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.32  
   19.33  schematic_lemma "?p : ~~P & ~~(P --> Q) --> ~~Q"
   19.34 -  by (tactic {* IntPr.fast_tac 1 *})
   19.35 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.36  
   19.37  
   19.38  subsection {* The following are classically but not constructively valid *}
   19.39  
   19.40  (*The attempt to prove them terminates quickly!*)
   19.41  schematic_lemma "?p : ((P-->Q) --> P)  -->  P"
   19.42 -  apply (tactic {* IntPr.fast_tac 1 *})?
   19.43 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   19.44    oops
   19.45  
   19.46  schematic_lemma "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)"
   19.47 -  apply (tactic {* IntPr.fast_tac 1 *})?
   19.48 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   19.49    oops
   19.50  
   19.51  
   19.52 @@ -71,74 +71,74 @@
   19.53  
   19.54  text "Problem ~~1"
   19.55  schematic_lemma "?p : ~~((P-->Q)  <->  (~Q --> ~P))"
   19.56 -  by (tactic {* IntPr.fast_tac 1 *})
   19.57 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.58  
   19.59  text "Problem ~~2"
   19.60  schematic_lemma "?p : ~~(~~P  <->  P)"
   19.61 -  by (tactic {* IntPr.fast_tac 1 *})
   19.62 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.63  
   19.64  text "Problem 3"
   19.65  schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
   19.66 -  by (tactic {* IntPr.fast_tac 1 *})
   19.67 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.68  
   19.69  text "Problem ~~4"
   19.70  schematic_lemma "?p : ~~((~P-->Q)  <->  (~Q --> P))"
   19.71 -  by (tactic {* IntPr.fast_tac 1 *})
   19.72 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.73  
   19.74  text "Problem ~~5"
   19.75  schematic_lemma "?p : ~~((P|Q-->P|R) --> P|(Q-->R))"
   19.76 -  by (tactic {* IntPr.fast_tac 1 *})
   19.77 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.78  
   19.79  text "Problem ~~6"
   19.80  schematic_lemma "?p : ~~(P | ~P)"
   19.81 -  by (tactic {* IntPr.fast_tac 1 *})
   19.82 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.83  
   19.84  text "Problem ~~7"
   19.85  schematic_lemma "?p : ~~(P | ~~~P)"
   19.86 -  by (tactic {* IntPr.fast_tac 1 *})
   19.87 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.88  
   19.89  text "Problem ~~8.  Peirce's law"
   19.90  schematic_lemma "?p : ~~(((P-->Q) --> P)  -->  P)"
   19.91 -  by (tactic {* IntPr.fast_tac 1 *})
   19.92 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.93  
   19.94  text "Problem 9"
   19.95  schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   19.96 -  by (tactic {* IntPr.fast_tac 1 *})
   19.97 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   19.98  
   19.99  text "Problem 10"
  19.100  schematic_lemma "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
  19.101 -  by (tactic {* IntPr.fast_tac 1 *})
  19.102 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.103  
  19.104  text "11.  Proved in each direction (incorrectly, says Pelletier!!) "
  19.105  schematic_lemma "?p : P<->P"
  19.106 -  by (tactic {* IntPr.fast_tac 1 *})
  19.107 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.108  
  19.109  text "Problem ~~12.  Dijkstra's law  "
  19.110  schematic_lemma "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
  19.111 -  by (tactic {* IntPr.fast_tac 1 *})
  19.112 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.113  
  19.114  schematic_lemma "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
  19.115 -  by (tactic {* IntPr.fast_tac 1 *})
  19.116 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.117  
  19.118  text "Problem 13.  Distributive law"
  19.119  schematic_lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
  19.120 -  by (tactic {* IntPr.fast_tac 1 *})
  19.121 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.122  
  19.123  text "Problem ~~14"
  19.124  schematic_lemma "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
  19.125 -  by (tactic {* IntPr.fast_tac 1 *})
  19.126 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.127  
  19.128  text "Problem ~~15"
  19.129  schematic_lemma "?p : ~~((P --> Q) <-> (~P | Q))"
  19.130 -  by (tactic {* IntPr.fast_tac 1 *})
  19.131 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.132  
  19.133  text "Problem ~~16"
  19.134  schematic_lemma "?p : ~~((P-->Q) | (Q-->P))"
  19.135 -  by (tactic {* IntPr.fast_tac 1 *})
  19.136 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.137  
  19.138  text "Problem ~~17"
  19.139  schematic_lemma "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
  19.140 -  by (tactic {* IntPr.fast_tac 1 *})  -- slow
  19.141 +  by (tactic {* IntPr.fast_tac @{context} 1 *})  -- slow
  19.142  
  19.143  
  19.144  subsection {* Examples with quantifiers *}
  19.145 @@ -146,43 +146,43 @@
  19.146  text "The converse is classical in the following implications..."
  19.147  
  19.148  schematic_lemma "?p : (EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
  19.149 -  by (tactic {* IntPr.fast_tac 1 *})
  19.150 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.151  
  19.152  schematic_lemma "?p : ((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
  19.153 -  by (tactic {* IntPr.fast_tac 1 *})
  19.154 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.155  
  19.156  schematic_lemma "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
  19.157 -  by (tactic {* IntPr.fast_tac 1 *})
  19.158 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.159  
  19.160  schematic_lemma "?p : (ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
  19.161 -  by (tactic {* IntPr.fast_tac 1 *})
  19.162 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.163  
  19.164  schematic_lemma "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
  19.165 -  by (tactic {* IntPr.fast_tac 1 *})
  19.166 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.167  
  19.168  
  19.169  text "The following are not constructively valid!"
  19.170  text "The attempt to prove them terminates quickly!"
  19.171  
  19.172  schematic_lemma "?p : ((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
  19.173 -  apply (tactic {* IntPr.fast_tac 1 *})?
  19.174 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
  19.175    oops
  19.176  
  19.177  schematic_lemma "?p : (P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
  19.178 -  apply (tactic {* IntPr.fast_tac 1 *})?
  19.179 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
  19.180    oops
  19.181  
  19.182  schematic_lemma "?p : (ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
  19.183 -  apply (tactic {* IntPr.fast_tac 1 *})?
  19.184 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
  19.185    oops
  19.186  
  19.187  schematic_lemma "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
  19.188 -  apply (tactic {* IntPr.fast_tac 1 *})?
  19.189 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
  19.190    oops
  19.191  
  19.192  (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
  19.193  schematic_lemma "?p : EX x. Q(x) --> (ALL x. Q(x))"
  19.194 -  apply (tactic {* IntPr.fast_tac 1 *})?
  19.195 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
  19.196    oops
  19.197  
  19.198  
  19.199 @@ -204,7 +204,7 @@
  19.200  text "Problem 20"
  19.201  schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
  19.202      --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
  19.203 -  by (tactic {* IntPr.fast_tac 1 *})
  19.204 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.205  
  19.206  text "Problem 21"
  19.207  schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))" oops
  19.208 @@ -212,21 +212,21 @@
  19.209  
  19.210  text "Problem 22"
  19.211  schematic_lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
  19.212 -  by (tactic {* IntPr.fast_tac 1 *})
  19.213 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.214  
  19.215  text "Problem ~~23"
  19.216  schematic_lemma "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
  19.217 -  by (tactic {* IntPr.fast_tac 1 *})
  19.218 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  19.219  
  19.220  text "Problem 24"
  19.221  schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
  19.222       (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
  19.223      --> ~~(EX x. P(x)&R(x))"
  19.224  (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
  19.225 -  apply (tactic "IntPr.safe_tac")
  19.226 +  apply (tactic "IntPr.safe_tac @{context}")
  19.227    apply (erule impE)
  19.228 -   apply (tactic "IntPr.fast_tac 1")
  19.229 -  apply (tactic "IntPr.fast_tac 1")
  19.230 +   apply (tactic "IntPr.fast_tac @{context} 1")
  19.231 +  apply (tactic "IntPr.fast_tac @{context} 1")
  19.232    done
  19.233  
  19.234  text "Problem 25"
  19.235 @@ -235,72 +235,72 @@
  19.236          (ALL x. P(x) --> (M(x) & L(x))) &    
  19.237          ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))   
  19.238      --> (EX x. Q(x)&P(x))"
  19.239 -  by (tactic "IntPr.best_tac 1")
  19.240 +  by (tactic "IntPr.best_tac @{context} 1")
  19.241  
  19.242  text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
  19.243  schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
  19.244      --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
  19.245           (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
  19.246 -  by (tactic "IntPr.fast_tac 1")
  19.247 +  by (tactic "IntPr.fast_tac @{context} 1")
  19.248  
  19.249  text "Problem ~~30"
  19.250  schematic_lemma "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) &  
  19.251          (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
  19.252      --> (ALL x. ~~S(x))"
  19.253 -  by (tactic "IntPr.fast_tac 1")
  19.254 +  by (tactic "IntPr.fast_tac @{context} 1")
  19.255  
  19.256  text "Problem 31"
  19.257  schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
  19.258          (EX x. L(x) & P(x)) &  
  19.259          (ALL x. ~ R(x) --> M(x))   
  19.260      --> (EX x. L(x) & M(x))"
  19.261 -  by (tactic "IntPr.fast_tac 1")
  19.262 +  by (tactic "IntPr.fast_tac @{context} 1")
  19.263  
  19.264  text "Problem 32"
  19.265  schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
  19.266          (ALL x. S(x) & R(x) --> L(x)) &  
  19.267          (ALL x. M(x) --> R(x))   
  19.268      --> (ALL x. P(x) & M(x) --> L(x))"
  19.269 -  by (tactic "IntPr.best_tac 1") -- slow
  19.270 +  by (tactic "IntPr.best_tac @{context} 1") -- slow
  19.271  
  19.272  text "Problem 39"
  19.273  schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
  19.274 -  by (tactic "IntPr.best_tac 1")
  19.275 +  by (tactic "IntPr.best_tac @{context} 1")
  19.276  
  19.277  text "Problem 40.  AMENDED"
  19.278  schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
  19.279                ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
  19.280 -  by (tactic "IntPr.best_tac 1") -- slow
  19.281 +  by (tactic "IntPr.best_tac @{context} 1") -- slow
  19.282  
  19.283  text "Problem 44"
  19.284  schematic_lemma "?p : (ALL x. f(x) -->                                    
  19.285                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
  19.286                (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
  19.287                --> (EX x. j(x) & ~f(x))"
  19.288 -  by (tactic "IntPr.best_tac 1")
  19.289 +  by (tactic "IntPr.best_tac @{context} 1")
  19.290  
  19.291  text "Problem 48"
  19.292  schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
  19.293 -  by (tactic "IntPr.best_tac 1")
  19.294 +  by (tactic "IntPr.best_tac @{context} 1")
  19.295  
  19.296  text "Problem 51"
  19.297  schematic_lemma
  19.298      "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->   
  19.299       (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
  19.300 -  by (tactic "IntPr.best_tac 1") -- {*60 seconds*}
  19.301 +  by (tactic "IntPr.best_tac @{context} 1") -- {*60 seconds*}
  19.302  
  19.303  text "Problem 56"
  19.304  schematic_lemma "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
  19.305 -  by (tactic "IntPr.best_tac 1")
  19.306 +  by (tactic "IntPr.best_tac @{context} 1")
  19.307  
  19.308  text "Problem 57"
  19.309  schematic_lemma
  19.310      "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
  19.311       (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
  19.312 -  by (tactic "IntPr.best_tac 1")
  19.313 +  by (tactic "IntPr.best_tac @{context} 1")
  19.314  
  19.315  text "Problem 60"
  19.316  schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
  19.317 -  by (tactic "IntPr.best_tac 1")
  19.318 +  by (tactic "IntPr.best_tac @{context} 1")
  19.319  
  19.320  end
    20.1 --- a/src/FOLP/ex/Propositional_Int.thy	Sun Nov 09 20:49:28 2014 +0100
    20.2 +++ b/src/FOLP/ex/Propositional_Int.thy	Mon Nov 10 21:49:48 2014 +0100
    20.3 @@ -12,106 +12,106 @@
    20.4  
    20.5  text "commutative laws of & and | "
    20.6  schematic_lemma "?p : P & Q  -->  Q & P"
    20.7 -  by (tactic {* IntPr.fast_tac 1 *})
    20.8 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
    20.9  
   20.10  schematic_lemma "?p : P | Q  -->  Q | P"
   20.11 -  by (tactic {* IntPr.fast_tac 1 *})
   20.12 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.13  
   20.14  
   20.15  text "associative laws of & and | "
   20.16  schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
   20.17 -  by (tactic {* IntPr.fast_tac 1 *})
   20.18 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.19  
   20.20  schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
   20.21 -  by (tactic {* IntPr.fast_tac 1 *})
   20.22 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.23  
   20.24  
   20.25  text "distributive laws of & and | "
   20.26  schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   20.27 -  by (tactic {* IntPr.fast_tac 1 *})
   20.28 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.29  
   20.30  schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   20.31 -  by (tactic {* IntPr.fast_tac 1 *})
   20.32 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.33  
   20.34  schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   20.35 -  by (tactic {* IntPr.fast_tac 1 *})
   20.36 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.37  
   20.38  
   20.39  schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   20.40 -  by (tactic {* IntPr.fast_tac 1 *})
   20.41 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.42  
   20.43  
   20.44  text "Laws involving implication"
   20.45  
   20.46  schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   20.47 -  by (tactic {* IntPr.fast_tac 1 *})
   20.48 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.49  
   20.50  schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   20.51 -  by (tactic {* IntPr.fast_tac 1 *})
   20.52 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.53  
   20.54  schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   20.55 -  by (tactic {* IntPr.fast_tac 1 *})
   20.56 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.57  
   20.58  schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   20.59 -  by (tactic {* IntPr.fast_tac 1 *})
   20.60 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.61  
   20.62  schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   20.63 -  by (tactic {* IntPr.fast_tac 1 *})
   20.64 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.65  
   20.66  
   20.67  text "Propositions-as-types"
   20.68  
   20.69  (*The combinator K*)
   20.70  schematic_lemma "?p : P --> (Q --> P)"
   20.71 -  by (tactic {* IntPr.fast_tac 1 *})
   20.72 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.73  
   20.74  (*The combinator S*)
   20.75  schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   20.76 -  by (tactic {* IntPr.fast_tac 1 *})
   20.77 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.78  
   20.79  
   20.80  (*Converse is classical*)
   20.81  schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   20.82 -  by (tactic {* IntPr.fast_tac 1 *})
   20.83 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.84  
   20.85  schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
   20.86 -  by (tactic {* IntPr.fast_tac 1 *})
   20.87 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.88  
   20.89  
   20.90  text "Schwichtenberg's examples (via T. Nipkow)"
   20.91  
   20.92  schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   20.93 -  by (tactic {* IntPr.fast_tac 1 *})
   20.94 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   20.95  
   20.96  schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   20.97                --> ((P --> Q) --> P) --> P"
   20.98 -  by (tactic {* IntPr.fast_tac 1 *})
   20.99 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  20.100  
  20.101  schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  20.102                 --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
  20.103 -  by (tactic {* IntPr.fast_tac 1 *})
  20.104 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  20.105    
  20.106  schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  20.107 -  by (tactic {* IntPr.fast_tac 1 *})
  20.108 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  20.109  
  20.110  schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  20.111 -  by (tactic {* IntPr.fast_tac 1 *})
  20.112 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  20.113  
  20.114  schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  20.115 -  by (tactic {* IntPr.fast_tac 1 *})
  20.116 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  20.117  
  20.118  schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  20.119            --> (((P8 --> P2) --> P9) --> P3 --> P10)  
  20.120            --> (P1 --> P8) --> P6 --> P7  
  20.121            --> (((P3 --> P2) --> P9) --> P4)  
  20.122            --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
  20.123 -  by (tactic {* IntPr.fast_tac 1 *})
  20.124 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  20.125  
  20.126  schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  20.127       --> (((P3 --> P2) --> P9) --> P4)  
  20.128       --> (((P6 --> P1) --> P2) --> P9)  
  20.129       --> (((P7 --> P1) --> P10) --> P4 --> P5)  
  20.130       --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
  20.131 -  by (tactic {* IntPr.fast_tac 1 *})
  20.132 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  20.133  
  20.134  end
    21.1 --- a/src/FOLP/ex/Quantifiers_Int.thy	Sun Nov 09 20:49:28 2014 +0100
    21.2 +++ b/src/FOLP/ex/Quantifiers_Int.thy	Mon Nov 10 21:49:48 2014 +0100
    21.3 @@ -11,91 +11,91 @@
    21.4  begin
    21.5  
    21.6  schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    21.7 -  by (tactic {* IntPr.fast_tac 1 *})
    21.8 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
    21.9  
   21.10  schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   21.11 -  by (tactic {* IntPr.fast_tac 1 *})
   21.12 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.13  
   21.14  
   21.15  (*Converse is false*)
   21.16  schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   21.17 -  by (tactic {* IntPr.fast_tac 1 *})
   21.18 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.19  
   21.20  schematic_lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   21.21 -  by (tactic {* IntPr.fast_tac 1 *})
   21.22 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.23  
   21.24  
   21.25  schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   21.26 -  by (tactic {* IntPr.fast_tac 1 *})
   21.27 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.28  
   21.29  
   21.30  text "Some harder ones"
   21.31  
   21.32  schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   21.33 -  by (tactic {* IntPr.fast_tac 1 *})
   21.34 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.35  
   21.36  (*Converse is false*)
   21.37  schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   21.38 -  by (tactic {* IntPr.fast_tac 1 *})
   21.39 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.40  
   21.41  
   21.42  text "Basic test of quantifier reasoning"
   21.43  (*TRUE*)
   21.44  schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   21.45 -  by (tactic {* IntPr.fast_tac 1 *})
   21.46 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.47  
   21.48  schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   21.49 -  by (tactic {* IntPr.fast_tac 1 *})
   21.50 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.51  
   21.52  
   21.53  text "The following should fail, as they are false!"
   21.54  
   21.55  schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   21.56 -  apply (tactic {* IntPr.fast_tac 1 *})?
   21.57 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   21.58    oops
   21.59  
   21.60  schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   21.61 -  apply (tactic {* IntPr.fast_tac 1 *})?
   21.62 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   21.63    oops
   21.64  
   21.65  schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
   21.66 -  apply (tactic {* IntPr.fast_tac 1 *})?
   21.67 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   21.68    oops
   21.69  
   21.70  schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   21.71 -  apply (tactic {* IntPr.fast_tac 1 *})?
   21.72 +  apply (tactic {* IntPr.fast_tac @{context} 1 *})?
   21.73    oops
   21.74  
   21.75  
   21.76  text "Back to things that are provable..."
   21.77  
   21.78  schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   21.79 -  by (tactic {* IntPr.fast_tac 1 *})
   21.80 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.81  
   21.82  
   21.83  (*An example of why exI should be delayed as long as possible*)
   21.84  schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   21.85 -  by (tactic {* IntPr.fast_tac 1 *})
   21.86 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.87  
   21.88  schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   21.89 -  by (tactic {* IntPr.fast_tac 1 *})
   21.90 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.91  
   21.92  schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   21.93 -  by (tactic {* IntPr.fast_tac 1 *})
   21.94 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
   21.95  
   21.96  
   21.97  text "Some slow ones"
   21.98  
   21.99  (*Principia Mathematica *11.53  *)
  21.100  schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  21.101 -  by (tactic {* IntPr.fast_tac 1 *})
  21.102 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  21.103  
  21.104  (*Principia Mathematica *11.55  *)
  21.105  schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  21.106 -  by (tactic {* IntPr.fast_tac 1 *})
  21.107 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  21.108  
  21.109  (*Principia Mathematica *11.61  *)
  21.110  schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  21.111 -  by (tactic {* IntPr.fast_tac 1 *})
  21.112 +  by (tactic {* IntPr.fast_tac @{context} 1 *})
  21.113  
  21.114  end
    22.1 --- a/src/FOLP/intprover.ML	Sun Nov 09 20:49:28 2014 +0100
    22.2 +++ b/src/FOLP/intprover.ML	Mon Nov 10 21:49:48 2014 +0100
    22.3 @@ -15,13 +15,13 @@
    22.4  
    22.5  signature INT_PROVER = 
    22.6    sig
    22.7 -  val best_tac: int -> tactic
    22.8 -  val fast_tac: int -> tactic
    22.9 -  val inst_step_tac: int -> tactic
   22.10 -  val safe_step_tac: int -> tactic
   22.11 +  val best_tac: Proof.context -> int -> tactic
   22.12 +  val fast_tac: Proof.context -> int -> tactic
   22.13 +  val inst_step_tac: Proof.context -> int -> tactic
   22.14 +  val safe_step_tac: Proof.context -> int -> tactic
   22.15    val safe_brls: (bool * thm) list
   22.16 -  val safe_tac: tactic
   22.17 -  val step_tac: int -> tactic
   22.18 +  val safe_tac: Proof.context -> tactic
   22.19 +  val step_tac: Proof.context -> int -> tactic
   22.20    val haz_brls: (bool * thm) list
   22.21    end;
   22.22  
   22.23 @@ -52,26 +52,26 @@
   22.24      List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
   22.25  
   22.26  (*Attack subgoals using safe inferences*)
   22.27 -val safe_step_tac = FIRST' [uniq_assume_tac,
   22.28 -                            int_uniq_mp_tac,
   22.29 +fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt,
   22.30 +                            int_uniq_mp_tac ctxt,
   22.31                              biresolve_tac safe0_brls,
   22.32                              hyp_subst_tac,
   22.33                              biresolve_tac safep_brls] ;
   22.34  
   22.35  (*Repeatedly attack subgoals using safe inferences*)
   22.36 -val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
   22.37 +fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt));
   22.38  
   22.39  (*These steps could instantiate variables and are therefore unsafe.*)
   22.40 -val inst_step_tac = assume_tac APPEND' mp_tac;
   22.41 +fun inst_step_tac ctxt = assume_tac ctxt APPEND' mp_tac ctxt;
   22.42  
   22.43  (*One safe or unsafe step. *)
   22.44 -fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
   22.45 +fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_brls i];
   22.46  
   22.47  (*Dumb but fast*)
   22.48 -val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
   22.49 +fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
   22.50  
   22.51  (*Slower but smarter than fast_tac*)
   22.52 -val best_tac = 
   22.53 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
   22.54 +fun best_tac ctxt =
   22.55 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
   22.56  
   22.57  end;
    23.1 --- a/src/FOLP/simp.ML	Sun Nov 09 20:49:28 2014 +0100
    23.2 +++ b/src/FOLP/simp.ML	Mon Nov 10 21:49:48 2014 +0100
    23.3 @@ -451,7 +451,7 @@
    23.4                       thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
    23.5              end
    23.6      | NONE => if more
    23.7 -            then rew((lhs_net_tac anet i THEN assume_tac i) thm,
    23.8 +            then rew((lhs_net_tac anet i THEN atac i) thm,
    23.9                       thm,ss,anet,ats,cs,false)
   23.10              else (ss,thm,anet,ats,cs);
   23.11  
    24.1 --- a/src/HOL/Auth/Event.thy	Sun Nov 09 20:49:28 2014 +0100
    24.2 +++ b/src/HOL/Auth/Event.thy	Mon Nov 10 21:49:48 2014 +0100
    24.3 @@ -270,14 +270,14 @@
    24.4  
    24.5  ML
    24.6  {*
    24.7 -val analz_mono_contra_tac = 
    24.8 +fun analz_mono_contra_tac ctxt = 
    24.9    rtac @{thm analz_impI} THEN' 
   24.10    REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
   24.11 -  THEN' mp_tac
   24.12 +  THEN' (mp_tac ctxt)
   24.13  *}
   24.14  
   24.15  method_setup analz_mono_contra = {*
   24.16 -    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
   24.17 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
   24.18      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   24.19  
   24.20  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
   24.21 @@ -286,7 +286,7 @@
   24.22  
   24.23  ML
   24.24  {*
   24.25 -val synth_analz_mono_contra_tac = 
   24.26 +fun synth_analz_mono_contra_tac ctxt = 
   24.27    rtac @{thm syan_impI} THEN'
   24.28    REPEAT1 o 
   24.29      (dresolve_tac 
   24.30 @@ -294,11 +294,11 @@
   24.31        @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
   24.32        @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])
   24.33    THEN'
   24.34 -  mp_tac
   24.35 +  mp_tac ctxt
   24.36  *}
   24.37  
   24.38  method_setup synth_analz_mono_contra = {*
   24.39 -    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
   24.40 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (synth_analz_mono_contra_tac ctxt))) *}
   24.41      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
   24.42  
   24.43  end
    25.1 --- a/src/HOL/Auth/Recur.thy	Sun Nov 09 20:49:28 2014 +0100
    25.2 +++ b/src/HOL/Auth/Recur.thy	Mon Nov 10 21:49:48 2014 +0100
    25.3 @@ -163,7 +163,7 @@
    25.4                                    [THEN respond.Cons, THEN respond.Cons]],
    25.5                       THEN recur.RA4, THEN recur.RA4])
    25.6  apply basic_possibility
    25.7 -apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
    25.8 +apply (tactic "DEPTH_SOLVE (swap_res_tac @{context} [refl, conjI, disjCI] 1)")
    25.9  done
   25.10  
   25.11  
    26.1 --- a/src/HOL/Bali/AxSem.thy	Sun Nov 09 20:49:28 2014 +0100
    26.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Nov 10 21:49:48 2014 +0100
    26.3 @@ -661,13 +661,14 @@
    26.4  lemma ax_thin [rule_format (no_asm)]: 
    26.5    "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
    26.6  apply (erule ax_derivs.induct)
    26.7 -apply                (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
    26.8 +apply                (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1])")
    26.9  apply                (rule ax_derivs.empty)
   26.10  apply               (erule (1) ax_derivs.insert)
   26.11  apply              (fast intro: ax_derivs.asm)
   26.12  (*apply           (fast intro: ax_derivs.cut) *)
   26.13  apply            (fast intro: ax_derivs.weaken)
   26.14 -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) 
   26.15 +apply           (rule ax_derivs.conseq, intro strip, tactic "smp_tac @{context} 3 1",clarify,
   26.16 +  tactic "smp_tac @{context} 1 1",rule exI, rule exI, erule (1) conjI) 
   26.17  (* 37 subgoals *)
   26.18  prefer 18 (* Methd *)
   26.19  apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
   26.20 @@ -700,7 +701,7 @@
   26.21  apply     (fast intro: ax_derivs.asm)
   26.22  (*apply  (blast intro: ax_derivs.cut) *)
   26.23  apply   (fast intro: ax_derivs.weaken)
   26.24 -apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
   26.25 +apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac @{context} 3 1", blast(* unused *))
   26.26  (*37 subgoals*)
   26.27  apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros}) 
   26.28                     THEN_ALL_NEW fast_tac @{context}) *})
    27.1 --- a/src/HOL/Bali/AxSound.thy	Sun Nov 09 20:49:28 2014 +0100
    27.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Nov 10 21:49:48 2014 +0100
    27.3 @@ -50,13 +50,13 @@
    27.4  apply (rule iffI)
    27.5  apply  fast
    27.6  apply clarify
    27.7 -apply (tactic "smp_tac 3 1")
    27.8 +apply (tactic "smp_tac @{context} 3 1")
    27.9  apply (case_tac "normal s")
   27.10  apply  clarsimp
   27.11  apply  (elim conjE impE)
   27.12  apply    blast
   27.13  
   27.14 -apply    (tactic "smp_tac 2 1")
   27.15 +apply    (tactic "smp_tac @{context} 2 1")
   27.16  apply    (drule evaln_eval)
   27.17  apply    (drule (1) eval_type_sound [THEN conjunct1],simp, assumption+)
   27.18  apply    simp
   27.19 @@ -84,7 +84,7 @@
   27.20  "\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk> 
   27.21    \<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
   27.22  apply (simp (no_asm_use) add: triple_valid2_def2)
   27.23 -apply (intro strip, tactic "smp_tac 3 1", clarify)
   27.24 +apply (intro strip, tactic "smp_tac @{context} 3 1", clarify)
   27.25  apply (erule wt_elim_cases, erule da_elim_cases, erule evaln_elim_cases)
   27.26  apply (unfold body_def Let_def)
   27.27  apply (clarsimp simp add: inj_term_simps)
   27.28 @@ -400,14 +400,14 @@
   27.29        from valid_A conf wt da eval P con
   27.30        have "Q v s1 Z"
   27.31          apply (simp add: ax_valids2_def triple_valid2_def2)
   27.32 -        apply (tactic "smp_tac 3 1")
   27.33 +        apply (tactic "smp_tac @{context} 3 1")
   27.34          apply clarify
   27.35 -        apply (tactic "smp_tac 1 1")
   27.36 +        apply (tactic "smp_tac @{context} 1 1")
   27.37          apply (erule allE,erule allE, erule mp)
   27.38          apply (intro strip)
   27.39 -        apply (tactic "smp_tac 3 1")
   27.40 -        apply (tactic "smp_tac 2 1")
   27.41 -        apply (tactic "smp_tac 1 1")
   27.42 +        apply (tactic "smp_tac @{context} 3 1")
   27.43 +        apply (tactic "smp_tac @{context} 2 1")
   27.44 +        apply (tactic "smp_tac @{context} 1 1")
   27.45          by blast
   27.46        moreover have "s1\<Colon>\<preceq>(G, L)"
   27.47        proof (cases "normal s0")
   27.48 @@ -2065,7 +2065,7 @@
   27.49                            (abupd (absorb (Cont l')) s2') \<diamondsuit> s3'"
   27.50                    apply (simp only: True if_True eqs)
   27.51                    apply (elim conjE)
   27.52 -                  apply (tactic "smp_tac 3 1")
   27.53 +                  apply (tactic "smp_tac @{context} 3 1")
   27.54                    apply fast
   27.55                    done
   27.56                  from eval_e
    28.1 --- a/src/HOL/Bali/Evaln.thy	Sun Nov 09 20:49:28 2014 +0100
    28.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Nov 10 21:49:48 2014 +0100
    28.3 @@ -449,7 +449,7 @@
    28.4    "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')"
    28.5  apply (erule evaln.induct)
    28.6  apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
    28.7 -  REPEAT o smp_tac 1, 
    28.8 +  REPEAT o smp_tac @{context} 1, 
    28.9    resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
   28.10  (* 3 subgoals *)
   28.11  apply (auto split del: split_if)
    29.1 --- a/src/HOL/Bali/Table.thy	Sun Nov 09 20:49:28 2014 +0100
    29.2 +++ b/src/HOL/Bali/Table.thy	Mon Nov 10 21:49:48 2014 +0100
    29.3 @@ -396,7 +396,7 @@
    29.4  apply (rename_tac "ba")
    29.5  apply (drule_tac x = "ba" in spec)
    29.6  apply clarify
    29.7 -apply (tactic "smp_tac 2 1")
    29.8 +apply (tactic "smp_tac @{context} 2 1")
    29.9  apply (erule (1) notE impE)
   29.10  apply (case_tac "aa = b")
   29.11  apply fast+
    30.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Nov 09 20:49:28 2014 +0100
    30.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Mon Nov 10 21:49:48 2014 +0100
    30.3 @@ -80,7 +80,7 @@
    30.4         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
    30.5         TRY (simp_tac simpset3 1), TRY (simp_tac (put_simpset cooper_ss ctxt) 1)]
    30.6        (Thm.trivial ct))
    30.7 -    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    30.8 +    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
    30.9      (* The result of the quantifier elimination *)
   30.10      val (th, tac) =
   30.11        (case (prop_of pre_thm) of
    31.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Nov 09 20:49:28 2014 +0100
    31.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Mon Nov 10 21:49:48 2014 +0100
    31.3 @@ -61,7 +61,7 @@
    31.4        [simp_tac simpset0 1,
    31.5         TRY (simp_tac (put_simpset ferrack_ss ctxt) 1)]
    31.6        (Thm.trivial ct))
    31.7 -    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    31.8 +    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
    31.9      (* The result of the quantifier elimination *)
   31.10      val (th, tac) = case prop_of pre_thm of
   31.11          Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    32.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Nov 09 20:49:28 2014 +0100
    32.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon Nov 10 21:49:48 2014 +0100
    32.3 @@ -108,7 +108,7 @@
    32.4         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
    32.5         TRY (simp_tac (put_simpset mir_ss ctxt) 1)]
    32.6        (Thm.trivial ct))
    32.7 -    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    32.8 +    fun assm_tac i = REPEAT_DETERM_N nh (assume_tac ctxt i)
    32.9      (* The result of the quantifier elimination *)
   32.10      val (th, tac) = case (prop_of pre_thm) of
   32.11          Const (@{const_name Pure.imp}, _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
    33.1 --- a/src/HOL/HOL.thy	Sun Nov 09 20:49:28 2014 +0100
    33.2 +++ b/src/HOL/HOL.thy	Mon Nov 10 21:49:48 2014 +0100
    33.3 @@ -1982,7 +1982,7 @@
    33.4      val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
    33.5    in
    33.6      fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
    33.7 -    fun smp_tac j = EVERY'[dresolve_tac (smp j), assume_tac];
    33.8 +    fun smp_tac ctxt j = EVERY'[dresolve_tac (smp j), assume_tac ctxt];
    33.9    end;
   33.10  
   33.11    local
    34.1 --- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Sun Nov 09 20:49:28 2014 +0100
    34.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Mon Nov 10 21:49:48 2014 +0100
    34.3 @@ -199,7 +199,7 @@
    34.4  apply (drule spec, erule impE)
    34.5  apply  (erule BufAC_Asm_antiton [THEN antitonPD])
    34.6  apply  (erule is_ub_thelub)
    34.7 -apply (tactic "smp_tac 3 1")
    34.8 +apply (tactic "smp_tac @{context} 3 1")
    34.9  apply (drule is_ub_thelub)
   34.10  apply (drule (1) mp)
   34.11  apply (drule (1) mp)
    35.1 --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Sun Nov 09 20:49:28 2014 +0100
    35.2 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Mon Nov 10 21:49:48 2014 +0100
    35.3 @@ -777,7 +777,7 @@
    35.4  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    35.5  apply(tactic {* TRYALL (etac disjE) *})
    35.6  apply simp_all
    35.7 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
    35.8 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *})
    35.9  apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}]) *})
   35.10  apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
   35.11  done
    36.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Sun Nov 09 20:49:28 2014 +0100
    36.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Nov 10 21:49:48 2014 +0100
    36.3 @@ -1187,7 +1187,7 @@
    36.4  --{* 72 subgoals left *}
    36.5  apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    36.6  --{* 35 subgoals left *}
    36.7 -apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
    36.8 +apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}]) *})
    36.9  --{* 28 subgoals left *}
   36.10  apply(tactic {* TRYALL (etac conjE) *})
   36.11  apply(tactic {* TRYALL (etac disjE) *})
    37.1 --- a/src/HOL/IMPP/Hoare.thy	Sun Nov 09 20:49:28 2014 +0100
    37.2 +++ b/src/HOL/IMPP/Hoare.thy	Mon Nov 10 21:49:48 2014 +0100
    37.3 @@ -209,13 +209,13 @@
    37.4  *)
    37.5  lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
    37.6  apply (erule hoare_derivs.induct)
    37.7 -apply                (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1]) *})
    37.8 +apply                (tactic {* ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
    37.9  apply (rule hoare_derivs.empty)
   37.10  apply               (erule (1) hoare_derivs.insert)
   37.11  apply              (fast intro: hoare_derivs.asm)
   37.12  apply             (fast intro: hoare_derivs.cut)
   37.13  apply            (fast intro: hoare_derivs.weaken)
   37.14 -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)
   37.15 +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)
   37.16  prefer 7
   37.17  apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
   37.18  apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *})
   37.19 @@ -287,9 +287,9 @@
   37.20  apply        (blast) (* weaken *)
   37.21  apply       (tactic {* ALLGOALS (EVERY'
   37.22    [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
   37.23 -   simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac 1]) *})
   37.24 +   simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
   37.25  apply       (simp_all (no_asm_use) add: triple_valid_def2)
   37.26 -apply       (intro strip, tactic "smp_tac 2 1", blast) (* conseq *)
   37.27 +apply       (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *)
   37.28  apply      (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *)
   37.29  prefer 3 apply   (force) (* Call *)
   37.30  apply  (erule_tac [2] evaln_elim_cases) (* If *)
    38.1 --- a/src/HOL/IMPP/Misc.thy	Sun Nov 09 20:49:28 2014 +0100
    38.2 +++ b/src/HOL/IMPP/Misc.thy	Mon Nov 10 21:49:48 2014 +0100
    38.3 @@ -71,12 +71,12 @@
    38.4  apply (simp (no_asm_use) add: triple_valid_def2)
    38.5  apply clarsimp
    38.6  apply (drule_tac x = "s<Y>" in spec)
    38.7 -apply (tactic "smp_tac 1 1")
    38.8 +apply (tactic "smp_tac @{context} 1 1")
    38.9  apply (drule spec)
   38.10  apply (drule_tac x = "s[Loc Y::=a s]" in spec)
   38.11  apply (simp (no_asm_use))
   38.12  apply (erule (1) notE impE)
   38.13 -apply (tactic "smp_tac 1 1")
   38.14 +apply (tactic "smp_tac @{context} 1 1")
   38.15  apply simp
   38.16  done
   38.17  
    39.1 --- a/src/HOL/IMPP/Natural.thy	Sun Nov 09 20:49:28 2014 +0100
    39.2 +++ b/src/HOL/IMPP/Natural.thy	Mon Nov 10 21:49:48 2014 +0100
    39.3 @@ -139,7 +139,8 @@
    39.4  lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
    39.5  apply (erule evalc.induct)
    39.6  apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
    39.7 -apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac, REPEAT o eresolve_tac [exE, conjE]]) *})
    39.8 +apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac @{context},
    39.9 +  REPEAT o eresolve_tac [exE, conjE]]) *})
   39.10  apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
   39.11  done
   39.12  
    40.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Sun Nov 09 20:49:28 2014 +0100
    40.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Nov 10 21:49:48 2014 +0100
    40.3 @@ -138,7 +138,7 @@
    40.4  apply( drule (3) Call_lemma)
    40.5  apply( clarsimp simp add: wf_java_mdecl_def)
    40.6  apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
    40.7 -apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac 2")
    40.8 +apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
    40.9  apply(  rule conformsI)
   40.10  apply(   erule conforms_heapD)
   40.11  apply(  rule lconf_ext)
   40.12 @@ -156,10 +156,10 @@
   40.13  apply(  fast intro: hext_trans)
   40.14  apply( rule conjI)
   40.15  apply(  rule_tac [2] impI)
   40.16 -apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
   40.17 +apply(  erule_tac [2] notE impE, tactic "assume_tac @{context} 2")
   40.18  apply(  frule_tac [2] conf_widen)
   40.19 -apply(    tactic "assume_tac 4")
   40.20 -apply(   tactic "assume_tac 2")
   40.21 +apply(    tactic "assume_tac @{context} 4")
   40.22 +apply(   tactic "assume_tac @{context} 2")
   40.23  prefer 2
   40.24  apply(  fast elim!: widen_trans)
   40.25  apply (rule conforms_xcpt_change)
   40.26 @@ -177,8 +177,9 @@
   40.27  declare wf_prog_ws_prog [simp]
   40.28  
   40.29  ML{*
   40.30 -val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
   40.31 -  (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
   40.32 +fun forward_hyp_tac ctxt =
   40.33 +  ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac ctxt,
   40.34 +    (mp_tac ctxt ORELSE' (dtac spec THEN' mp_tac ctxt)), REPEAT o (etac conjE)]))
   40.35  *}
   40.36  
   40.37  
   40.38 @@ -226,8 +227,8 @@
   40.39  apply( erule conf_litval)
   40.40  
   40.41  -- "13 BinOp"
   40.42 -apply (tactic "forward_hyp_tac")
   40.43 -apply (tactic "forward_hyp_tac")
   40.44 +apply (tactic "forward_hyp_tac @{context}")
   40.45 +apply (tactic "forward_hyp_tac @{context}")
   40.46  apply( rule conjI, erule (1) hext_trans)
   40.47  apply( erule conjI)
   40.48  apply( clarsimp)
   40.49 @@ -246,7 +247,7 @@
   40.50  apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW
   40.51    (asm_full_simp_tac @{context})) 7*})
   40.52  
   40.53 -apply (tactic "forward_hyp_tac")
   40.54 +apply (tactic "forward_hyp_tac @{context}")
   40.55  
   40.56  -- "11+1 if"
   40.57  prefer 7
   40.58 @@ -294,7 +295,7 @@
   40.59  apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
   40.60  apply(force elim: hext_trans)
   40.61  
   40.62 -apply (tactic "forward_hyp_tac")
   40.63 +apply (tactic "forward_hyp_tac @{context}")
   40.64  
   40.65  -- "4 Cond"
   40.66  prefer 4
   40.67 @@ -317,7 +318,7 @@
   40.68  apply( case_tac "x2")
   40.69    -- "x2 = None"
   40.70    apply (simp)
   40.71 -  apply (tactic forward_hyp_tac, clarify)
   40.72 +  apply (tactic "forward_hyp_tac @{context}", clarify)
   40.73    apply( drule eval_no_xcpt)
   40.74    apply( erule FAss_type_sound, rule HOL.refl, assumption+)
   40.75    -- "x2 = Some a"
    41.1 --- a/src/HOL/NanoJava/AxSem.thy	Sun Nov 09 20:49:28 2014 +0100
    41.2 +++ b/src/HOL/NanoJava/AxSem.thy	Mon Nov 10 21:49:48 2014 +0100
    41.3 @@ -152,7 +152,7 @@
    41.4    "(A' |\<turnstile>  C         \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile>  C       )) \<and> 
    41.5     (A'  \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A  \<turnstile>\<^sub>e {P} e {Q}))"
    41.6  apply (rule hoare_ehoare.induct)
    41.7 -apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
    41.8 +apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac @{context} 1])")
    41.9  apply (blast intro: hoare_ehoare.Skip)
   41.10  apply (blast intro: hoare_ehoare.Comp)
   41.11  apply (blast intro: hoare_ehoare.Cond)
   41.12 @@ -164,7 +164,7 @@
   41.13  apply (blast intro: hoare_ehoare.NewC)
   41.14  apply (blast intro: hoare_ehoare.Cast)
   41.15  apply (erule hoare_ehoare.Call)
   41.16 -apply   (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption)
   41.17 +apply   (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption)
   41.18  apply  blast
   41.19  apply (blast intro!: hoare_ehoare.Meth)
   41.20  apply (blast intro!: hoare_ehoare.Impl)
   41.21 @@ -172,9 +172,9 @@
   41.22  apply (blast intro: hoare_ehoare.ConjI)
   41.23  apply (blast intro: hoare_ehoare.ConjE)
   41.24  apply (rule hoare_ehoare.Conseq)
   41.25 -apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
   41.26 +apply  (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption+)
   41.27  apply (rule hoare_ehoare.eConseq)
   41.28 -apply  (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+)
   41.29 +apply  (rule, drule spec, erule conjE, tactic "smp_tac @{context} 1 1", assumption+)
   41.30  done
   41.31  
   41.32  lemma cThin: "\<lbrakk>A' |\<turnstile> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
    42.1 --- a/src/HOL/NanoJava/Equivalence.thy	Sun Nov 09 20:49:28 2014 +0100
    42.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Mon Nov 10 21:49:48 2014 +0100
    42.3 @@ -111,7 +111,7 @@
    42.4                   apply fast
    42.5                  apply fast
    42.6                 apply fast
    42.7 -              apply (clarify,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
    42.8 +              apply (clarify,tactic "smp_tac @{context} 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
    42.9               apply fast
   42.10              apply fast
   42.11             apply fast
    43.1 --- a/src/HOL/NanoJava/Example.thy	Sun Nov 09 20:49:28 2014 +0100
    43.2 +++ b/src/HOL/NanoJava/Example.thy	Mon Nov 10 21:49:48 2014 +0100
    43.3 @@ -131,7 +131,7 @@
    43.4  apply  auto
    43.5  apply  (case_tac "aa=a")
    43.6  apply   auto
    43.7 -apply (tactic "smp_tac 1 1")
    43.8 +apply (tactic "smp_tac @{context} 1 1")
    43.9  apply (case_tac "aa=a")
   43.10  apply  auto
   43.11  done
    44.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 09 20:49:28 2014 +0100
    44.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Nov 10 21:49:48 2014 +0100
    44.3 @@ -438,11 +438,11 @@
    44.4          in
    44.5            fold (fn (s, tvs) => fn thy => Axclass.prove_arity
    44.6                (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
    44.7 -              (fn _ => EVERY
    44.8 +              (fn ctxt => EVERY
    44.9                  [Class.intro_classes_tac [],
   44.10                   resolve_tac perm_empty_thms 1,
   44.11                   resolve_tac perm_append_thms 1,
   44.12 -                 resolve_tac perm_eq_thms 1, assume_tac 1]) thy)
   44.13 +                 resolve_tac perm_eq_thms 1, assume_tac ctxt 1]) thy)
   44.14              (full_new_type_names' ~~ tyvars) thy
   44.15          end) atoms |>
   44.16        Global_Theory.add_thmss
   44.17 @@ -562,7 +562,7 @@
   44.18             [Old_Datatype_Aux.ind_tac rep_induct [] 1,
   44.19              ALLGOALS (simp_tac (ctxt addsimps
   44.20                (Thm.symmetric perm_fun_def :: abs_perm))),
   44.21 -            ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
   44.22 +            ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac ctxt)])),
   44.23          length new_type_names));
   44.24  
   44.25      val perm_closed_thmss = map mk_perm_closed atoms;
   44.26 @@ -1721,9 +1721,9 @@
   44.27                        (S $ Free x $ Free y, P $ (Free y)))
   44.28                          (rec_unique_frees'' ~~ rec_unique_frees' ~~
   44.29                             rec_sets ~~ rec_preds)))))
   44.30 -               (fn _ =>
   44.31 +               (fn {context = ctxt, ...} =>
   44.32                    rtac rec_induct 1 THEN
   44.33 -                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac) 1))));
   44.34 +                  REPEAT ((resolve_tac P_ind_ths THEN_ALL_NEW assume_tac ctxt) 1))));
   44.35             val rec_fin_supp_thms' = map
   44.36               (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths))
   44.37               (rec_fin_supp_thms ~~ finite_thss);
    45.1 --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun Nov 09 20:49:28 2014 +0100
    45.2 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Mon Nov 10 21:49:48 2014 +0100
    45.3 @@ -539,7 +539,7 @@
    45.4    Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
    45.5      (fn i =>
    45.6        EVERY [ftac @{thm Gets_certificate_valid} i,
    45.7 -             assume_tac i,
    45.8 +             assume_tac ctxt i,
    45.9               etac conjE i, REPEAT (hyp_subst_tac ctxt i)]))
   45.10  *}
   45.11  
    46.1 --- a/src/HOL/SET_Protocol/Event_SET.thy	Sun Nov 09 20:49:28 2014 +0100
    46.2 +++ b/src/HOL/SET_Protocol/Event_SET.thy	Mon Nov 10 21:49:48 2014 +0100
    46.3 @@ -182,14 +182,14 @@
    46.4  
    46.5  ML
    46.6  {*
    46.7 -val analz_mono_contra_tac = 
    46.8 +fun analz_mono_contra_tac ctxt = 
    46.9    rtac @{thm analz_impI} THEN' 
   46.10    REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
   46.11 -  THEN' mp_tac
   46.12 +  THEN' mp_tac ctxt
   46.13  *}
   46.14  
   46.15  method_setup analz_mono_contra = {*
   46.16 -    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
   46.17 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (REPEAT_FIRST (analz_mono_contra_tac ctxt))) *}
   46.18      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   46.19  
   46.20  end
    47.1 --- a/src/HOL/SET_Protocol/Purchase.thy	Sun Nov 09 20:49:28 2014 +0100
    47.2 +++ b/src/HOL/SET_Protocol/Purchase.thy	Mon Nov 10 21:49:48 2014 +0100
    47.3 @@ -483,7 +483,7 @@
    47.4    Args.goal_spec >> (fn quant =>
    47.5      fn ctxt => SIMPLE_METHOD'' quant (fn i =>
    47.6        EVERY [ftac @{thm Gets_certificate_valid} i,
    47.7 -             assume_tac i, REPEAT (hyp_subst_tac ctxt i)]))
    47.8 +             assume_tac ctxt i, REPEAT (hyp_subst_tac ctxt i)]))
    47.9  *}
   47.10  
   47.11  
    48.1 --- a/src/HOL/Set.thy	Sun Nov 09 20:49:28 2014 +0100
    48.2 +++ b/src/HOL/Set.thy	Mon Nov 10 21:49:48 2014 +0100
    48.3 @@ -383,7 +383,7 @@
    48.4  
    48.5  setup {*
    48.6    map_theory_claset (fn ctxt =>
    48.7 -    ctxt addbefore ("bspec", fn _ => dresolve_tac @{thms bspec} THEN' assume_tac))
    48.8 +    ctxt addbefore ("bspec", fn ctxt' => dresolve_tac @{thms bspec} THEN' assume_tac ctxt'))
    48.9  *}
   48.10  
   48.11  ML {*
    49.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun Nov 09 20:49:28 2014 +0100
    49.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Nov 10 21:49:48 2014 +0100
    49.3 @@ -227,7 +227,7 @@
    49.4    val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
    49.5    val fast_solver = mk_solver "fast_solver" (fn ctxt =>
    49.6      if Config.get ctxt config_fast_solver
    49.7 -    then assume_tac ORELSE' (etac notE)
    49.8 +    then assume_tac ctxt ORELSE' (etac notE)
    49.9      else K no_tac);
   49.10  *}
   49.11  
    50.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Nov 09 20:49:28 2014 +0100
    50.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Nov 10 21:49:48 2014 +0100
    50.3 @@ -2471,7 +2471,7 @@
    50.4          fun distinct_prems ctxt thm =
    50.5            Goal.prove (*no sorry*) ctxt [] []
    50.6              (thm |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies)
    50.7 -            (fn _ => HEADGOAL (cut_tac thm THEN' atac) THEN ALLGOALS eq_assume_tac);
    50.8 +            (fn _ => HEADGOAL (cut_tac thm THEN' assume_tac ctxt) THEN ALLGOALS eq_assume_tac);
    50.9  
   50.10          fun eq_ifIN _ [thm] = thm
   50.11            | eq_ifIN ctxt (thm :: thms) =
    51.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Sun Nov 09 20:49:28 2014 +0100
    51.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Mon Nov 10 21:49:48 2014 +0100
    51.3 @@ -44,7 +44,7 @@
    51.4        (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN'
    51.5           REPEAT_ALL_NEW (FIRST' [eresolve_tac C_IHs, eresolve_tac C_IH_monos,
    51.6             SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac @{thm order_refl},
    51.7 -           atac, resolve_tac co_inducts,
    51.8 +           assume_tac ctxt, resolve_tac co_inducts,
    51.9             resolve_tac C_IH_monos THEN' REPEAT_ALL_NEW (eresolve_tac nesting_rel_monos)])))
   51.10      co_inducts)
   51.11    end;
    52.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Sun Nov 09 20:49:28 2014 +0100
    52.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Nov 10 21:49:48 2014 +0100
    52.3 @@ -452,7 +452,7 @@
    52.4          val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
    52.5        in
    52.6          Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
    52.7 -          (K ((hyp_subst_tac lthy THEN' atac) 1))
    52.8 +          (K ((hyp_subst_tac lthy THEN' assume_tac lthy) 1))
    52.9          |> Thm.close_derivation
   52.10          |> singleton (Proof_Context.export names_lthy lthy)
   52.11        end;
   52.12 @@ -550,7 +550,7 @@
   52.13          val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
   52.14        in
   52.15          Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
   52.16 -          (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' atac) 1)
   52.17 +          (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
   52.18          |> Thm.close_derivation
   52.19          |> singleton (Proof_Context.export names_lthy lthy)
   52.20        end;
    53.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Nov 09 20:49:28 2014 +0100
    53.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Nov 10 21:49:48 2014 +0100
    53.3 @@ -394,7 +394,7 @@
    53.4          val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
    53.5        in
    53.6          Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
    53.7 -          (K ((hyp_subst_tac lthy THEN' atac) 1))
    53.8 +          (K ((hyp_subst_tac lthy THEN' assume_tac lthy) 1))
    53.9          |> Thm.close_derivation
   53.10          |> singleton (Proof_Context.export names_lthy lthy)
   53.11        end;
    54.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun Nov 09 20:49:28 2014 +0100
    54.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Nov 10 21:49:48 2014 +0100
    54.3 @@ -906,7 +906,7 @@
    54.4                    val thms =
    54.5                      @{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
    54.6                          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    54.7 -                          mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac)
    54.8 +                          mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL (assume_tac ctxt))
    54.9                          |> Thm.close_derivation
   54.10                          |> not triv ? perhaps (try (fn thm => refl RS thm)))
   54.11                        ms discD_thms sel_thmss trivs goals;
    55.1 --- a/src/HOL/Tools/Function/function_core.ML	Sun Nov 09 20:49:28 2014 +0100
    55.2 +++ b/src/HOL/Tools/Function/function_core.ML	Mon Nov 10 21:49:48 2014 +0100
    55.3 @@ -683,7 +683,7 @@
    55.4        subset_induct_rule
    55.5        |> Thm.forall_intr (cterm_of thy D)
    55.6        |> Thm.forall_elim (cterm_of thy acc_R)
    55.7 -      |> assume_tac 1 |> Seq.hd
    55.8 +      |> atac 1 |> Seq.hd
    55.9        |> (curry op COMP) (acc_downward
   55.10          |> (instantiate' [SOME (ctyp_of thy domT)]
   55.11               (map (SOME o cterm_of thy) [R, x, z]))
    56.1 --- a/src/HOL/Tools/Function/function_elims.ML	Sun Nov 09 20:49:28 2014 +0100
    56.2 +++ b/src/HOL/Tools/Function/function_elims.ML	Mon Nov 10 21:49:48 2014 +0100
    56.3 @@ -125,7 +125,7 @@
    56.4            REPEAT (eresolve_tac @{thms Pair_inject} i)
    56.5            THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
    56.6            THEN propagate_tac ctxt i
    56.7 -          THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i)
    56.8 +          THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i)
    56.9            THEN bool_subst_tac ctxt i;
   56.10  
   56.11        val elim_stripped =
    57.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sun Nov 09 20:49:28 2014 +0100
    57.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Mon Nov 10 21:49:48 2014 +0100
    57.3 @@ -396,6 +396,6 @@
    57.4  
    57.5  
    57.6  fun induction_schema_tac ctxt =
    57.7 -  mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
    57.8 +  mk_ind_tac (K all_tac) (assume_tac ctxt APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt;
    57.9  
   57.10  end
    58.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Sun Nov 09 20:49:28 2014 +0100
    58.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Mon Nov 10 21:49:48 2014 +0100
    58.3 @@ -32,8 +32,8 @@
    58.4    in
    58.5      EVERY' [SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Quotient_alt_def5}]), 
    58.6        REPEAT_DETERM o (etac conjE), rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_Grp_UNIV_sym]),
    58.7 -      rtac rel_mono THEN_ALL_NEW atac, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
    58.8 -        [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW atac,
    58.9 +      rtac rel_mono THEN_ALL_NEW assume_tac ctxt, rtac conjI, SELECT_GOAL (Local_Defs.unfold_tac ctxt
   58.10 +        [rel_conversep_sym, rel_Grp_UNIV_sym]), rtac rel_mono THEN_ALL_NEW assume_tac ctxt,
   58.11        SELECT_GOAL (Local_Defs.unfold_tac ctxt [rel_conversep_sym, rel_OO_of_bnf bnf RS sym]),
   58.12        hyp_subst_tac ctxt, rtac refl] i
   58.13    end
    59.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 20:49:28 2014 +0100
    59.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Nov 10 21:49:48 2014 +0100
    59.3 @@ -30,8 +30,8 @@
    59.4    val make_clauses_unsorted: Proof.context -> thm list -> thm list
    59.5    val make_clauses: Proof.context -> thm list -> thm list
    59.6    val make_horns: thm list -> thm list
    59.7 -  val best_prolog_tac: (thm -> int) -> thm list -> tactic
    59.8 -  val depth_prolog_tac: thm list -> tactic
    59.9 +  val best_prolog_tac: Proof.context -> (thm -> int) -> thm list -> tactic
   59.10 +  val depth_prolog_tac: Proof.context -> thm list -> tactic
   59.11    val gocls: thm list -> thm list
   59.12    val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
   59.13    val MESON:
   59.14 @@ -503,8 +503,8 @@
   59.15  
   59.16  
   59.17  (* net_resolve_tac actually made it slower... *)
   59.18 -fun prolog_step_tac horns i =
   59.19 -    (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
   59.20 +fun prolog_step_tac ctxt horns i =
   59.21 +    (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN
   59.22      TRYALL_eq_assume_tac;
   59.23  
   59.24  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   59.25 @@ -690,11 +690,11 @@
   59.26  (*Could simply use nprems_of, which would count remaining subgoals -- no
   59.27    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
   59.28  
   59.29 -fun best_prolog_tac sizef horns =
   59.30 -    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
   59.31 +fun best_prolog_tac ctxt sizef horns =
   59.32 +    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1);
   59.33  
   59.34 -fun depth_prolog_tac horns =
   59.35 -    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
   59.36 +fun depth_prolog_tac ctxt horns =
   59.37 +    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1);
   59.38  
   59.39  (*Return all negative clauses, as possible goal clauses*)
   59.40  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
   59.41 @@ -723,7 +723,7 @@
   59.42      (fn cls =>
   59.43           THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
   59.44                           (has_fewer_prems 1, sizef)
   59.45 -                         (prolog_step_tac (make_horns cls) 1))
   59.46 +                         (prolog_step_tac ctxt (make_horns cls) 1))
   59.47      ctxt
   59.48  
   59.49  (*First, breaks the goal into independent units*)
   59.50 @@ -734,7 +734,7 @@
   59.51  
   59.52  fun depth_meson_tac ctxt =
   59.53    MESON all_tac (make_clauses ctxt)
   59.54 -    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)])
   59.55 +    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)])
   59.56      ctxt
   59.57  
   59.58  (** Iterative deepening version **)
   59.59 @@ -747,7 +747,7 @@
   59.60          val nrtac = net_resolve_tac horns
   59.61      in  fn i => eq_assume_tac i ORELSE
   59.62                  match_tac ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   59.63 -                ((assume_tac i APPEND nrtac i) THEN check_tac)
   59.64 +                ((assume_tac ctxt i APPEND nrtac i) THEN check_tac)
   59.65      end;
   59.66  
   59.67  fun iter_deepen_prolog_tac ctxt horns =
    60.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Nov 09 20:49:28 2014 +0100
    60.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Nov 10 21:49:48 2014 +0100
    60.3 @@ -439,7 +439,10 @@
    60.4          val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
    60.5          val goal = Logic.list_implies (prems, concl)
    60.6          val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
    60.7 -        val tac = cut_tac th 1 THEN rewrite_goals_tac ctxt' meta_not_not THEN ALLGOALS assume_tac
    60.8 +        val tac =
    60.9 +          cut_tac th 1 THEN
   60.10 +          rewrite_goals_tac ctxt' meta_not_not THEN
   60.11 +          ALLGOALS (assume_tac ctxt')
   60.12        in
   60.13          if length prems = length prems0 then
   60.14            raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
   60.15 @@ -746,7 +749,7 @@
   60.16              THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
   60.17                THEN rotate_tac (rotation_of_subgoal i) i
   60.18                THEN PRIMITIVE (unify_first_prem_with_concl thy i)
   60.19 -              THEN assume_tac i
   60.20 +              THEN assume_tac ctxt' i
   60.21                THEN flexflex_tac ctxt')))
   60.22        handle ERROR msg =>
   60.23          cat_error msg
    61.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sun Nov 09 20:49:28 2014 +0100
    61.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Nov 10 21:49:48 2014 +0100
    61.3 @@ -382,8 +382,8 @@
    61.4                     (map (pair "x") Ts, S $ Old_Datatype_Aux.app_bnds f i)),
    61.5                   HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (Term.abs o pair "x") Ts
    61.6                     (r $ (a $ Old_Datatype_Aux.app_bnds f i)), f))))
    61.7 -              (fn _ => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
    61.8 -                 REPEAT (etac allE 1), rtac thm 1, atac 1])
    61.9 +              (fn {context = ctxt, ...} => EVERY [REPEAT_DETERM_N i (rtac @{thm ext} 1),
   61.10 +                 REPEAT (etac allE 1), rtac thm 1, assume_tac ctxt 1])
   61.11            end
   61.12        in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
   61.13  
   61.14 @@ -431,12 +431,12 @@
   61.15                         [REPEAT (eresolve_tac (Scons_inject ::
   61.16                            map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
   61.17                          REPEAT (cong_tac ctxt 1), rtac refl 1,
   61.18 -                        REPEAT (atac 1 ORELSE (EVERY
   61.19 +                        REPEAT (assume_tac ctxt 1 ORELSE (EVERY
   61.20                            [REPEAT (rtac @{thm ext} 1),
   61.21                             REPEAT (eresolve_tac (mp :: allE ::
   61.22                               map make_elim (Suml_inject :: Sumr_inject ::
   61.23                                 Lim_inject :: inj_thms') @ fun_congs) 1),
   61.24 -                           atac 1]))])])])]);
   61.25 +                           assume_tac ctxt 1]))])])])]);
   61.26  
   61.27          val inj_thms'' = map (fn r => r RS datatype_injI) (Old_Datatype_Aux.split_conj_thm inj_thm);
   61.28  
   61.29 @@ -565,7 +565,7 @@
   61.30               REPEAT (eresolve_tac inj_thms 1),
   61.31               REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac @{thm ext} 1),
   61.32                 REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
   61.33 -               atac 1]))])
   61.34 +               assume_tac ctxt 1]))])
   61.35        end;
   61.36  
   61.37      val constr_inject =
    62.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sun Nov 09 20:49:28 2014 +0100
    62.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Nov 10 21:49:48 2014 +0100
    62.3 @@ -183,7 +183,7 @@
    62.4                  REPEAT_DETERM_N j distinct_tac,
    62.5                  TRY (dresolve_tac inject 1),
    62.6                  REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1,
    62.7 -                REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac 1]),
    62.8 +                REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac ctxt 1]),
    62.9                  TRY (hyp_subst_tac ctxt 1),
   62.10                  resolve_tac [refl] 1,
   62.11                  REPEAT_DETERM_N (n - j - 1) distinct_tac],
    63.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Nov 09 20:49:28 2014 +0100
    63.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Nov 10 21:49:48 2014 +0100
    63.3 @@ -171,8 +171,8 @@
    63.4                THEN EVERY1 (select_disj (length disjuncts) (index + 1)) 
    63.5                THEN (EVERY (map (fn y =>
    63.6                  rtac (Drule.cterm_instantiate [(x, cterm_of thy (Free y))] @{thm exI}) 1) ps))
    63.7 -              THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN atac 1)
    63.8 -              THEN TRY (atac 1)
    63.9 +              THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
   63.10 +              THEN TRY (assume_tac ctxt' 1)
   63.11            in
   63.12              Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac)
   63.13            end
    64.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Sun Nov 09 20:49:28 2014 +0100
    64.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Mon Nov 10 21:49:48 2014 +0100
    64.3 @@ -78,7 +78,7 @@
    64.4      THEN trace_tac ctxt options "prove_param"
    64.5      THEN f_tac
    64.6      THEN trace_tac ctxt options "after prove_param"
    64.7 -    THEN (REPEAT_DETERM (atac 1))
    64.8 +    THEN (REPEAT_DETERM (assume_tac ctxt 1))
    64.9      THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
   64.10      THEN REPEAT_DETERM (rtac @{thm refl} 1)
   64.11    end
   64.12 @@ -97,11 +97,11 @@
   64.13          THEN trace_tac ctxt options "after intro rule"
   64.14          (* for the right assumption in first position *)
   64.15          THEN rotate_tac premposition 1
   64.16 -        THEN atac 1
   64.17 +        THEN assume_tac ctxt 1
   64.18          THEN trace_tac ctxt options "parameter goal"
   64.19          (* work with parameter arguments *)
   64.20          THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
   64.21 -        THEN (REPEAT_DETERM (atac 1))
   64.22 +        THEN (REPEAT_DETERM (assume_tac ctxt 1))
   64.23        end
   64.24    | (Free _, _) =>
   64.25        trace_tac ctxt options "proving parameter call.."
   64.26 @@ -242,7 +242,7 @@
   64.27                        THEN rtac (nth prems premposition) 1) ctxt 1
   64.28                      THEN trace_tac ctxt options "after applying not introduction rule"
   64.29                      THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
   64.30 -                    THEN (REPEAT_DETERM (atac 1))
   64.31 +                    THEN (REPEAT_DETERM (assume_tac ctxt 1))
   64.32                    else
   64.33                      rtac @{thm not_predI'} 1
   64.34                      (* test: *)
   64.35 @@ -410,8 +410,10 @@
   64.36          THEN (rtac pred_intro_rule
   64.37          (* How to handle equality correctly? *)
   64.38          THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
   64.39 -        THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac)))
   64.40 -          THEN' (K (trace_tac ctxt options "state after pre-simplification:"))
   64.41 +        THEN' (assume_tac ctxt ORELSE'
   64.42 +          ((CHANGED o asm_full_simp_tac split_simpset) THEN'
   64.43 +            (TRY o assume_tac ctxt))) THEN'
   64.44 +          (K (trace_tac ctxt options "state after pre-simplification:"))
   64.45          THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1))
   64.46      | prove_prems2 out_ts ((p, deriv) :: ps) =
   64.47        let
    65.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Nov 09 20:49:28 2014 +0100
    65.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Nov 10 21:49:48 2014 +0100
    65.3 @@ -396,7 +396,7 @@
    65.4                   RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
    65.5  
    65.6      (* resolving with R x y assumptions *)
    65.7 -    atac,
    65.8 +    assume_tac ctxt,
    65.9  
   65.10      (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
   65.11      rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
   65.12 @@ -560,7 +560,7 @@
   65.13        val concl' = apply_under_Trueprop (all_list vrs) concl
   65.14        val goal = Logic.mk_implies (concl', concl)
   65.15        val rule = Goal.prove ctxt [] [] goal
   65.16 -        (K (EVERY1 [inst_spec_tac (rev cvrs), atac]))
   65.17 +        (K (EVERY1 [inst_spec_tac (rev cvrs), assume_tac ctxt]))
   65.18      in
   65.19        rtac rule i
   65.20      end)
    66.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Sun Nov 09 20:49:28 2014 +0100
    66.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Mon Nov 10 21:49:48 2014 +0100
    66.3 @@ -51,7 +51,7 @@
    66.4  
    66.5  
    66.6  (* tactic to prove the quot_type theorem for the new type *)
    66.7 -fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
    66.8 +fun typedef_quot_type_tac ctxt equiv_thm ((_, typedef_info): Typedef.info) =
    66.9    let
   66.10      val rep_thm = #Rep typedef_info RS mem_def1
   66.11      val rep_inv = #Rep_inverse typedef_info
   66.12 @@ -62,7 +62,7 @@
   66.13        rtac equiv_thm,
   66.14        rtac rep_thm,
   66.15        rtac rep_inv,
   66.16 -      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
   66.17 +      rtac abs_inv THEN' rtac mem_def2 THEN' assume_tac ctxt,
   66.18        rtac rep_inj]) 1
   66.19    end
   66.20  
   66.21 @@ -74,7 +74,7 @@
   66.22      val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
   66.23    in
   66.24      Goal.prove lthy [] [] goal
   66.25 -      (K (typedef_quot_type_tac equiv_thm typedef_info))
   66.26 +      (fn {context = ctxt, ...} => typedef_quot_type_tac ctxt equiv_thm typedef_info)
   66.27    end
   66.28     
   66.29  open Lifting_Util
    67.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Sun Nov 09 20:49:28 2014 +0100
    67.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Mon Nov 10 21:49:48 2014 +0100
    67.3 @@ -78,12 +78,13 @@
    67.4        rel_OO_of_bnf bnf]
    67.5    in
    67.6      (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
    67.7 -      THEN_ALL_NEW atac) i
    67.8 +      THEN_ALL_NEW assume_tac ctxt) i
    67.9    end
   67.10  
   67.11  fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
   67.12    (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
   67.13 -    CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
   67.14 +    CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW
   67.15 +      (REPEAT_DETERM o etac conjE THEN' assume_tac ctxt)) sided_constr_intros) i
   67.16  
   67.17  fun generate_relation_constraint_goal ctxt bnf constraint_def =
   67.18    let
   67.19 @@ -199,7 +200,8 @@
   67.20          in_rel_of_bnf bnf, pred_def]), rtac iffI,
   67.21          REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
   67.22          CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
   67.23 -          etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
   67.24 +          etac imageE, dtac set_rev_mp, assume_tac ctxt,
   67.25 +          REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
   67.26            hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
   67.27            etac @{thm DomainPI}]) set_map's,
   67.28          REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
   67.29 @@ -209,7 +211,8 @@
   67.30            rtac @{thm fst_conv}]), rtac CollectI,
   67.31          CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
   67.32            REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
   67.33 -          dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
   67.34 +          dtac (rotate_prems 1 bspec), assume_tac ctxt,
   67.35 +          etac @{thm DomainpE}, etac @{thm someI}]) set_map's
   67.36        ] i
   67.37    end
   67.38  
    68.1 --- a/src/HOL/Tools/cnf.ML	Sun Nov 09 20:49:28 2014 +0100
    68.2 +++ b/src/HOL/Tools/cnf.ML	Mon Nov 10 21:49:48 2014 +0100
    68.3 @@ -42,7 +42,7 @@
    68.4    val clause2raw_thm: thm -> thm
    68.5    val make_nnf_thm: theory -> term -> thm
    68.6  
    68.7 -  val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
    68.8 +  val weakening_tac: Proof.context -> int -> tactic  (* removes the first hypothesis of a subgoal *)
    68.9  
   68.10    val make_cnf_thm: Proof.context -> term -> thm
   68.11    val make_cnfx_thm: Proof.context -> term -> thm
   68.12 @@ -528,8 +528,8 @@
   68.13  (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
   68.14  (* ------------------------------------------------------------------------- *)
   68.15  
   68.16 -fun weakening_tac i =
   68.17 -  dresolve_tac [weakening_thm] i THEN assume_tac (i+1);
   68.18 +fun weakening_tac ctxt i =
   68.19 +  dresolve_tac [weakening_thm] i THEN assume_tac ctxt (i+1);
   68.20  
   68.21  (* ------------------------------------------------------------------------- *)
   68.22  (* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF       *)
   68.23 @@ -551,7 +551,7 @@
   68.24      let
   68.25        val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   68.26      in
   68.27 -      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   68.28 +      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac ctxt 1)) thm
   68.29      end) i;
   68.30  
   68.31  (* ------------------------------------------------------------------------- *)
   68.32 @@ -573,7 +573,7 @@
   68.33      let
   68.34        val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
   68.35      in
   68.36 -      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
   68.37 +      PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac ctxt 1)) thm
   68.38      end) i;
   68.39  
   68.40  end;
    69.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Nov 09 20:49:28 2014 +0100
    69.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Mon Nov 10 21:49:48 2014 +0100
    69.3 @@ -118,7 +118,7 @@
    69.4              ALLGOALS (Object_Logic.atomize_prems_tac ctxt),
    69.5              rewrite_goals_tac ctxt (@{thm o_def} :: map mk_meta_eq rec_rewrites),
    69.6              REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
    69.7 -              REPEAT (etac allE i) THEN atac i)) 1)])
    69.8 +              REPEAT (etac allE i) THEN assume_tac ctxt i)) 1)])
    69.9        |> Drule.export_without_context;
   69.10  
   69.11      val ind_name = Thm.derivation_name induct;
    70.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 09 20:49:28 2014 +0100
    70.2 +++ b/src/HOL/Tools/inductive.ML	Mon Nov 10 21:49:48 2014 +0100
    70.3 @@ -381,7 +381,7 @@
    70.4      (fn _ => EVERY [resolve_tac @{thms monoI} 1,
    70.5        REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
    70.6        REPEAT (FIRST
    70.7 -        [assume_tac 1,
    70.8 +        [assume_tac ctxt 1,
    70.9           resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
   70.10           eresolve_tac @{thms le_funE} 1,
   70.11           dresolve_tac @{thms le_boolD} 1])]));
   70.12 @@ -406,7 +406,7 @@
   70.13          EVERY1 (select_disj (length intr_ts) (i + 1)),
   70.14          (*Not ares_tac, since refl must be tried before any equality assumptions;
   70.15            backtracking may occur if the premises have extra variables!*)
   70.16 -        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
   70.17 +        DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac ctxt 1)])
   70.18         |> singleton (Proof_Context.export ctxt ctxt')) intr_ts
   70.19  
   70.20    in (intrs, unfold) end;
   70.21 @@ -544,7 +544,7 @@
   70.22  
   70.23  (*delete needless equality assumptions*)
   70.24  val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
   70.25 -  (fn _ => assume_tac 1);
   70.26 +  (fn {context = ctxt, ...} => assume_tac ctxt 1);
   70.27  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
   70.28  val elim_tac = REPEAT o eresolve_tac elim_rls;
   70.29  
   70.30 @@ -741,7 +741,7 @@
   70.31             some premise involves disjunction.*)
   70.32           REPEAT (FIRSTGOAL (eresolve_tac [conjE] ORELSE' bound_hyp_subst_tac ctxt3)),
   70.33           REPEAT (FIRSTGOAL
   70.34 -           (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac))),
   70.35 +           (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac ctxt3))),
   70.36           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
   70.37               (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
   70.38             conjI, refl] 1)) prems)]);
   70.39 @@ -752,9 +752,9 @@
   70.40           REPEAT (EVERY
   70.41             [REPEAT (resolve_tac [conjI, impI] 1),
   70.42              REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
   70.43 -            assume_tac 1,
   70.44 +            assume_tac ctxt3 1,
   70.45              rewrite_goals_tac ctxt3 simp_thms1,
   70.46 -            assume_tac 1])]);
   70.47 +            assume_tac ctxt3 1])]);
   70.48  
   70.49    in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
   70.50  
    71.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Nov 09 20:49:28 2014 +0100
    71.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Mon Nov 10 21:49:48 2014 +0100
    71.3 @@ -397,7 +397,7 @@
    71.4             rewrite_goals_tac ctxt rews,
    71.5             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
    71.6               [K (rewrite_goals_tac ctxt rews), Object_Logic.atomize_prems_tac ctxt,
    71.7 -              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
    71.8 +              DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE]]) 1)]);
    71.9          val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
   71.10            (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
   71.11          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
   71.12 @@ -460,7 +460,7 @@
   71.13               ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt)),
   71.14               rewrite_goals_tac ctxt rews,
   71.15               REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac ctxt THEN'
   71.16 -               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   71.17 +               DEPTH_SOLVE_1 o FIRST' [assume_tac ctxt, etac allE, etac impE])) 1)]);
   71.18          val (thm', thy') = Global_Theory.store_thm (Binding.qualified_name (space_implode "_"
   71.19            (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
   71.20        in
    72.1 --- a/src/HOL/Tools/record.ML	Sun Nov 09 20:49:28 2014 +0100
    72.2 +++ b/src/HOL/Tools/record.ML	Mon Nov 10 21:49:48 2014 +0100
    72.3 @@ -1625,9 +1625,9 @@
    72.4          (fn {context = ctxt, ...} =>
    72.5            EVERY1
    72.6             [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt,
    72.7 -            etac @{thm meta_allE}, atac,
    72.8 +            etac @{thm meta_allE}, assume_tac ctxt,
    72.9              rtac (@{thm prop_subst} OF [surject]),
   72.10 -            REPEAT o etac @{thm meta_allE}, atac]));
   72.11 +            REPEAT o etac @{thm meta_allE}, assume_tac ctxt]));
   72.12  
   72.13      val induct = timeit_msg ctxt "record extension induct proof:" (fn () =>
   72.14        let val (assm, concl) = induct_prop in
   72.15 @@ -2160,9 +2160,9 @@
   72.16          (fn {context = ctxt', ...} =>
   72.17            EVERY1
   72.18             [rtac @{thm equal_intr_rule}, Goal.norm_hhf_tac ctxt',
   72.19 -            etac @{thm meta_allE}, atac,
   72.20 +            etac @{thm meta_allE}, assume_tac ctxt',
   72.21              rtac (@{thm prop_subst} OF [surjective]),
   72.22 -            REPEAT o etac @{thm meta_allE}, atac]));
   72.23 +            REPEAT o etac @{thm meta_allE}, assume_tac ctxt']));
   72.24  
   72.25      val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
   72.26        Goal.prove_sorry_global defs_thy [] [] split_object_prop
    73.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Nov 09 20:49:28 2014 +0100
    73.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Nov 10 21:49:48 2014 +0100
    73.3 @@ -344,7 +344,7 @@
    73.4      THEN' resolve_tac @{thms UnI2}
    73.5      THEN' tac1_of_formula ctxt fm2
    73.6    | tac1_of_formula ctxt (Atom _) =
    73.7 -    REPEAT_DETERM1 o (assume_tac
    73.8 +    REPEAT_DETERM1 o (assume_tac ctxt
    73.9        ORELSE' resolve_tac @{thms SigmaI}
   73.10        ORELSE' ((resolve_tac @{thms CollectI} ORELSE' resolve_tac [collectI']) THEN'
   73.11          TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
   73.12 @@ -356,7 +356,7 @@
   73.13        ORELSE' resolve_tac @{thms arg_cong2[OF refl, where f = "op =", OF prod.case, THEN iffD2]})))
   73.14        ORELSE' resolve_tac @{thms UNIV_I}
   73.15        ORELSE' resolve_tac @{thms iffD2[OF Compl_iff]}
   73.16 -      ORELSE' assume_tac)
   73.17 +      ORELSE' assume_tac ctxt)
   73.18  
   73.19  fun tac2_of_formula ctxt (Int (fm1, fm2)) =
   73.20      TRY o eresolve_tac @{thms IntE}
   73.21 @@ -370,7 +370,7 @@
   73.22      THEN' tac2_of_formula ctxt fm2
   73.23    | tac2_of_formula ctxt (Atom _) =
   73.24      REPEAT_DETERM o
   73.25 -      (assume_tac
   73.26 +      (assume_tac ctxt
   73.27         ORELSE' dresolve_tac @{thms iffD1[OF mem_Sigma_iff]}
   73.28         ORELSE' eresolve_tac @{thms conjE}
   73.29         ORELSE' ((eresolve_tac @{thms CollectE} ORELSE' eresolve_tac [collectE']) THEN'
   73.30 @@ -434,14 +434,14 @@
   73.31        THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
   73.32        THEN' resolve_tac @{thms iffI}
   73.33        THEN' REPEAT_DETERM o resolve_tac @{thms exI}
   73.34 -      THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac
   73.35 +      THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac ctxt
   73.36        THEN' REPEAT_DETERM o eresolve_tac @{thms exE}
   73.37        THEN' eresolve_tac @{thms conjE}
   73.38        THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
   73.39        THEN' Subgoal.FOCUS (fn {prems, ...} =>
   73.40          (* FIXME inner context!? *)
   73.41          simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
   73.42 -      THEN' TRY o assume_tac
   73.43 +      THEN' TRY o assume_tac ctxt
   73.44    in
   73.45      case try mk_term (term_of ct) of
   73.46        NONE => Thm.reflexive ct
    74.1 --- a/src/HOL/Tools/simpdata.ML	Sun Nov 09 20:49:28 2014 +0100
    74.2 +++ b/src/HOL/Tools/simpdata.ML	Mon Nov 10 21:49:48 2014 +0100
    74.3 @@ -119,7 +119,7 @@
    74.4      val sol_thms =
    74.5        reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
    74.6      fun sol_tac i =
    74.7 -      FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
    74.8 +      FIRST [resolve_tac sol_thms i, assume_tac ctxt i , eresolve_tac @{thms FalseE} i] ORELSE
    74.9        (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
   74.10    in
   74.11      (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
    75.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Sun Nov 09 20:49:28 2014 +0100
    75.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Nov 10 21:49:48 2014 +0100
    75.3 @@ -713,7 +713,7 @@
    75.4    EVERY [
    75.5      simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
    75.6      rtac @{thm guarantees_PLam_I} 1,
    75.7 -    assume_tac 2,
    75.8 +    assume_tac ctxt 2,
    75.9           (*preserves: routine reasoning*)
   75.10      asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2,
   75.11           (*the guarantee for  "lift i (rename client_map Client)" *)
    76.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Sun Nov 09 20:49:28 2014 +0100
    76.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Nov 10 21:49:48 2014 +0100
    76.3 @@ -110,7 +110,7 @@
    76.4        full_simp_tac ctxt 1,
    76.5        REPEAT (FIRSTGOAL (etac disjE)),
    76.6        ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])),
    76.7 -      REPEAT (FIRSTGOAL analz_mono_contra_tac),
    76.8 +      REPEAT (FIRSTGOAL (analz_mono_contra_tac ctxt)),
    76.9        ALLGOALS (asm_simp_tac ctxt)]) i;
   76.10  
   76.11  (*Tactic for proving secrecy theorems*)
    77.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Sun Nov 09 20:49:28 2014 +0100
    77.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Mon Nov 10 21:49:48 2014 +0100
    77.3 @@ -6,7 +6,8 @@
    77.4  *)
    77.5  
    77.6  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
    77.7 -val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}
    77.8 +fun Always_Int_tac ctxt =
    77.9 +  dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin}
   77.10  
   77.11  (*Combines a list of invariance THEOREMS into one.*)
   77.12  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I})
   77.13 @@ -16,7 +17,7 @@
   77.14  fun constrains_tac ctxt i =
   77.15    SELECT_GOAL
   77.16      (EVERY
   77.17 -     [REPEAT (Always_Int_tac 1),
   77.18 +     [REPEAT (Always_Int_tac ctxt 1),
   77.19        (*reduce the fancy safety properties to "constrains"*)
   77.20        REPEAT (etac @{thm Always_ConstrainsI} 1
   77.21                ORELSE
   77.22 @@ -35,7 +36,7 @@
   77.23  fun ensures_tac ctxt sact =
   77.24    SELECT_GOAL
   77.25      (EVERY
   77.26 -     [REPEAT (Always_Int_tac 1),
   77.27 +     [REPEAT (Always_Int_tac ctxt 1),
   77.28        etac @{thm Always_LeadsTo_Basis} 1
   77.29            ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   77.30            REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    78.1 --- a/src/HOL/Word/Word.thy	Sun Nov 09 20:49:28 2014 +0100
    78.2 +++ b/src/HOL/Word/Word.thy	Mon Nov 10 21:49:48 2014 +0100
    78.3 @@ -1565,8 +1565,8 @@
    78.4        ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
    78.5                           REPEAT (etac conjE n) THEN
    78.6                           REPEAT (dtac @{thm word_of_int_inverse} n 
    78.7 -                                 THEN atac n 
    78.8 -                                 THEN atac n)),
    78.9 +                                 THEN assume_tac ctxt n 
   78.10 +                                 THEN assume_tac ctxt n)),
   78.11        TRYALL arith_tac' ]
   78.12    end
   78.13  
    79.1 --- a/src/HOL/ex/Meson_Test.thy	Sun Nov 09 20:49:28 2014 +0100
    79.2 +++ b/src/HOL/ex/Meson_Test.thy	Mon Nov 10 21:49:48 2014 +0100
    79.3 @@ -40,7 +40,7 @@
    79.4      val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt;
    79.5      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
    79.6        rtac go25 1 THEN
    79.7 -      Meson.depth_prolog_tac horns25);
    79.8 +      Meson.depth_prolog_tac ctxt' horns25);
    79.9    *}
   79.10    oops
   79.11  
   79.12 @@ -66,7 +66,7 @@
   79.13      val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt;
   79.14      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
   79.15        rtac go26 1 THEN
   79.16 -      Meson.depth_prolog_tac horns26);  (*7 ms*)
   79.17 +      Meson.depth_prolog_tac ctxt' horns26);  (*7 ms*)
   79.18      (*Proof is of length 107!!*)
   79.19    *}
   79.20    oops
   79.21 @@ -93,7 +93,7 @@
   79.22      val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt;
   79.23      Goal.prove ctxt' [] [] @{prop False} (fn _ =>
   79.24        rtac go43 1 THEN
   79.25 -      Meson.best_prolog_tac Meson.size_of_subgoals horns43);   (*7ms*)
   79.26 +      Meson.best_prolog_tac ctxt' Meson.size_of_subgoals horns43);   (*7ms*)
   79.27      *}
   79.28    oops
   79.29  
    80.1 --- a/src/Provers/blast.ML	Sun Nov 09 20:49:28 2014 +0100
    80.2 +++ b/src/Provers/blast.ML	Mon Nov 10 21:49:48 2014 +0100
    80.3 @@ -782,14 +782,14 @@
    80.4  
    80.5  (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
    80.6  fun contr_tac ctxt =
    80.7 -  ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac);
    80.8 +  ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac ctxt);
    80.9  
   80.10  (*Try to unify complementary literals and return the corresponding tactic. *)
   80.11  fun tryClose state (G, L) =
   80.12    let
   80.13      val State {ctxt, ...} = state;
   80.14      val eContr_tac = TRACE ctxt Data.notE contr_tac;
   80.15 -    val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac);
   80.16 +    val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac ctxt);
   80.17      fun close t u tac = if unify state ([], t, u) then SOME tac else NONE;
   80.18      fun arg (_ $ t) = t;
   80.19    in
    81.1 --- a/src/Provers/classical.ML	Sun Nov 09 20:49:28 2014 +0100
    81.2 +++ b/src/Provers/classical.ML	Mon Nov 10 21:49:48 2014 +0100
    81.3 @@ -71,14 +71,14 @@
    81.4    val depth_tac: Proof.context -> int -> int -> tactic
    81.5    val deepen_tac: Proof.context -> int -> int -> tactic
    81.6  
    81.7 -  val contr_tac: int -> tactic
    81.8 +  val contr_tac: Proof.context -> int -> tactic
    81.9    val dup_elim: Context.generic option -> thm -> thm
   81.10    val dup_intr: thm -> thm
   81.11    val dup_step_tac: Proof.context -> int -> tactic
   81.12    val eq_mp_tac: Proof.context -> int -> tactic
   81.13    val haz_step_tac: Proof.context -> int -> tactic
   81.14    val joinrules: thm list * thm list -> (bool * thm) list
   81.15 -  val mp_tac: int -> tactic
   81.16 +  val mp_tac: Proof.context -> int -> tactic
   81.17    val safe_tac: Proof.context -> tactic
   81.18    val safe_steps_tac: Proof.context -> int -> tactic
   81.19    val safe_step_tac: Proof.context -> int -> tactic
   81.20 @@ -87,7 +87,7 @@
   81.21    val step_tac: Proof.context -> int -> tactic
   81.22    val slow_step_tac: Proof.context -> int -> tactic
   81.23    val swapify: thm list -> thm list
   81.24 -  val swap_res_tac: thm list -> int -> tactic
   81.25 +  val swap_res_tac: Proof.context -> thm list -> int -> tactic
   81.26    val inst_step_tac: Proof.context -> int -> tactic
   81.27    val inst0_step_tac: Proof.context -> int -> tactic
   81.28    val instp_step_tac: Proof.context -> int -> tactic
   81.29 @@ -179,12 +179,12 @@
   81.30  (*Prove goal that assumes both P and ~P.
   81.31    No backtracking if it finds an equal assumption.  Perhaps should call
   81.32    ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
   81.33 -val contr_tac =
   81.34 -  eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac);
   81.35 +fun contr_tac ctxt =
   81.36 +  eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt);
   81.37  
   81.38  (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   81.39    Could do the same thing for P<->Q and P... *)
   81.40 -fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
   81.41 +fun mp_tac ctxt i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i;
   81.42  
   81.43  (*Like mp_tac but instantiates no variables*)
   81.44  fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
   81.45 @@ -195,10 +195,10 @@
   81.46  
   81.47  (*Uses introduction rules in the normal way, or on negated assumptions,
   81.48    trying rules in order. *)
   81.49 -fun swap_res_tac rls =
   81.50 +fun swap_res_tac ctxt rls =
   81.51    let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in
   81.52 -    assume_tac ORELSE'
   81.53 -    contr_tac ORELSE'
   81.54 +    assume_tac ctxt ORELSE'
   81.55 +    contr_tac ctxt ORELSE'
   81.56      biresolve_tac (fold_rev addrl rls [])
   81.57    end;
   81.58  
   81.59 @@ -693,9 +693,9 @@
   81.60    ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
   81.61  
   81.62  fun ctxt addD2 (name, thm) =
   81.63 -  ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
   81.64 +  ctxt addafter (name, fn ctxt' => dresolve_tac [thm] THEN' assume_tac ctxt');
   81.65  fun ctxt addE2 (name, thm) =
   81.66 -  ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
   81.67 +  ctxt addafter (name, fn ctxt' => eresolve_tac [thm] THEN' assume_tac ctxt');
   81.68  fun ctxt addSD2 (name, thm) =
   81.69    ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac);
   81.70  fun ctxt addSE2 (name, thm) =
   81.71 @@ -762,8 +762,8 @@
   81.72  (*Backtracking is allowed among the various these unsafe ways of
   81.73    proving a subgoal.  *)
   81.74  fun inst0_step_tac ctxt =
   81.75 -  assume_tac APPEND'
   81.76 -  contr_tac APPEND'
   81.77 +  assume_tac ctxt APPEND'
   81.78 +  contr_tac ctxt APPEND'
   81.79    biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
   81.80  
   81.81  (*These unsafe steps could generate more subgoals.*)
    82.1 --- a/src/Provers/typedsimp.ML	Sun Nov 09 20:49:28 2014 +0100
    82.2 +++ b/src/Provers/typedsimp.ML	Mon Nov 10 21:49:48 2014 +0100
    82.3 @@ -18,19 +18,19 @@
    82.4    (*Built-in rewrite rules*)
    82.5    val default_rls: thm list
    82.6    (*Type checking or similar -- solution of routine conditions*)
    82.7 -  val routine_tac: thm list -> int -> tactic
    82.8 +  val routine_tac: Proof.context -> thm list -> int -> tactic
    82.9    end;
   82.10  
   82.11  signature TSIMP =
   82.12    sig
   82.13 -  val asm_res_tac: thm list -> int -> tactic   
   82.14 -  val cond_norm_tac: ((int->tactic) * thm list * thm list) -> tactic
   82.15 -  val cond_step_tac: ((int->tactic) * thm list * thm list) -> int -> tactic
   82.16 -  val norm_tac: (thm list * thm list) -> tactic
   82.17 +  val asm_res_tac: Proof.context -> thm list -> int -> tactic   
   82.18 +  val cond_norm_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> tactic
   82.19 +  val cond_step_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> int -> tactic
   82.20 +  val norm_tac: Proof.context -> (thm list * thm list) -> tactic
   82.21    val process_rules: thm list -> thm list * thm list
   82.22    val rewrite_res_tac: int -> tactic   
   82.23    val split_eqn: thm
   82.24 -  val step_tac: (thm list * thm list) -> int -> tactic
   82.25 +  val step_tac: Proof.context -> (thm list * thm list) -> int -> tactic
   82.26    val subconv_res_tac: thm list -> int -> tactic   
   82.27    end;
   82.28  
   82.29 @@ -95,29 +95,29 @@
   82.30    ORELSE'  filt_resolve_tac [refl,refl_red] 1;
   82.31  
   82.32  (*Resolve with asms, whether rewrites or not*)
   82.33 -fun asm_res_tac asms =
   82.34 +fun asm_res_tac ctxt asms =
   82.35      let val (xsimp_rls,xother_rls) = process_rules asms
   82.36 -    in  routine_tac xother_rls  ORELSE'  
   82.37 +    in  routine_tac ctxt xother_rls  ORELSE'  
   82.38          filt_resolve_tac xsimp_rls 2
   82.39      end;
   82.40  
   82.41  (*Single step for simple rewriting*)
   82.42 -fun step_tac (congr_rls,asms) =
   82.43 -    asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
   82.44 +fun step_tac ctxt (congr_rls,asms) =
   82.45 +    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac  ORELSE'  
   82.46      subconv_res_tac congr_rls;
   82.47  
   82.48  (*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)
   82.49 -fun cond_step_tac (prove_cond_tac, congr_rls, asms) =
   82.50 -    asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
   82.51 +fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) =
   82.52 +    asm_res_tac ctxt asms   ORELSE'  rewrite_res_tac  ORELSE'  
   82.53      (resolve_tac [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'  
   82.54      subconv_res_tac congr_rls;
   82.55  
   82.56  (*Unconditional normalization tactic*)
   82.57 -fun norm_tac arg = REPEAT_FIRST (step_tac arg)  THEN
   82.58 +fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg)  THEN
   82.59      TRYALL (resolve_tac [red_if_equal]);
   82.60  
   82.61  (*Conditional normalization tactic*)
   82.62 -fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg)  THEN
   82.63 +fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg)  THEN
   82.64      TRYALL (resolve_tac [red_if_equal]);
   82.65  
   82.66  end;
    83.1 --- a/src/Pure/Isar/class_declaration.ML	Sun Nov 09 20:49:28 2014 +0100
    83.2 +++ b/src/Pure/Isar/class_declaration.ML	Mon Nov 10 21:49:48 2014 +0100
    83.3 @@ -97,7 +97,7 @@
    83.4      fun tac ctxt =
    83.5        REPEAT (SOMEGOAL
    83.6          (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
    83.7 -          ORELSE' assume_tac));
    83.8 +          ORELSE' assume_tac ctxt));
    83.9      val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
   83.10  
   83.11    in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
    84.1 --- a/src/Pure/Isar/method.ML	Sun Nov 09 20:49:28 2014 +0100
    84.2 +++ b/src/Pure/Isar/method.ML	Mon Nov 10 21:49:48 2014 +0100
    84.3 @@ -167,7 +167,7 @@
    84.4  in
    84.5  
    84.6  fun assm_tac ctxt =
    84.7 -  assume_tac APPEND'
    84.8 +  assume_tac ctxt APPEND'
    84.9    Goal.assume_rule_tac ctxt APPEND'
   84.10    cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
   84.11    cond_rtac (can Logic.dest_term) Drule.termI;
   84.12 @@ -211,7 +211,7 @@
   84.13    THEN_ALL_NEW Goal.norm_hhf_tac ctxt;
   84.14  
   84.15  fun gen_arule_tac tac ctxt j rules facts =
   84.16 -  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac);
   84.17 +  EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j (assume_tac ctxt));
   84.18  
   84.19  fun gen_some_rule_tac tac ctxt arg_rules facts = SUBGOAL (fn (goal, i) =>
   84.20    let
    85.1 --- a/src/Pure/Tools/rule_insts.ML	Sun Nov 09 20:49:28 2014 +0100
    85.2 +++ b/src/Pure/Tools/rule_insts.ML	Mon Nov 10 21:49:48 2014 +0100
    85.3 @@ -301,7 +301,7 @@
    85.4  fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve ctxt rule);
    85.5  
    85.6  (*forward tactic applies a rule to an assumption without deleting it*)
    85.7 -fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
    85.8 +fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac ctxt;
    85.9  
   85.10  (*dresolve tactic applies a rule to replace an assumption*)
   85.11  fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve ctxt rule);
    86.1 --- a/src/Pure/goal.ML	Sun Nov 09 20:49:28 2014 +0100
    86.2 +++ b/src/Pure/goal.ML	Mon Nov 10 21:49:48 2014 +0100
    86.3 @@ -336,7 +336,7 @@
    86.4      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
    86.5      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
    86.6      val tacs = Rs |> map (fn R =>
    86.7 -      eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac);
    86.8 +      eresolve_tac [Raw_Simplifier.norm_hhf ctxt (Thm.trivial R)] THEN_ALL_NEW assume_tac ctxt);
    86.9    in fold_rev (curry op APPEND') tacs (K no_tac) i end);
   86.10  
   86.11  end;
    87.1 --- a/src/Pure/simplifier.ML	Sun Nov 09 20:49:28 2014 +0100
    87.2 +++ b/src/Pure/simplifier.ML	Mon Nov 10 21:49:48 2014 +0100
    87.3 @@ -384,7 +384,7 @@
    87.4      val trivialities = Drule.reflexive_thm :: trivs;
    87.5  
    87.6      fun unsafe_solver_tac ctxt =
    87.7 -      FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac];
    87.8 +      FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
    87.9      val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
   87.10  
   87.11      (*no premature instantiation of variables during simplification*)
    88.1 --- a/src/Pure/tactic.ML	Sun Nov 09 20:49:28 2014 +0100
    88.2 +++ b/src/Pure/tactic.ML	Mon Nov 10 21:49:48 2014 +0100
    88.3 @@ -8,7 +8,7 @@
    88.4  sig
    88.5    val trace_goalno_tac: (int -> tactic) -> int -> tactic
    88.6    val rule_by_tactic: Proof.context -> tactic -> thm -> thm
    88.7 -  val assume_tac: int -> tactic
    88.8 +  val assume_tac: Proof.context -> int -> tactic
    88.9    val eq_assume_tac: int -> tactic
   88.10    val compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic
   88.11    val make_elim: thm -> thm
   88.12 @@ -101,7 +101,8 @@
   88.13       thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *)
   88.14  
   88.15  (*Solve subgoal i by assumption*)
   88.16 -fun assume_tac i = PRIMSEQ (Thm.assumption NONE i);
   88.17 +fun assume_tac ctxt i = PRIMSEQ (Thm.assumption (SOME ctxt) i);
   88.18 +fun atac i = PRIMSEQ (Thm.assumption NONE i);
   88.19  
   88.20  (*Solve subgoal i by assumption, using no unification*)
   88.21  fun eq_assume_tac i = PRIMITIVE (Thm.eq_assumption i);
   88.22 @@ -128,22 +129,21 @@
   88.23  fun eresolve_tac rules = biresolve_tac (map (pair true) rules);
   88.24  
   88.25  (*Forward reasoning using destruction rules.*)
   88.26 -fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac;
   88.27 +fun forward_tac rls = resolve_tac (map make_elim rls) THEN' atac;
   88.28  
   88.29  (*Like forward_tac, but deletes the assumption after use.*)
   88.30  fun dresolve_tac rls = eresolve_tac (map make_elim rls);
   88.31  
   88.32  (*Shorthand versions: for resolution with a single theorem*)
   88.33 -val atac    =   assume_tac;
   88.34  fun rtac rl =  resolve_tac [rl];
   88.35  fun dtac rl = dresolve_tac [rl];
   88.36  fun etac rl = eresolve_tac [rl];
   88.37  fun ftac rl =  forward_tac [rl];
   88.38  
   88.39  (*Use an assumption or some rules ... A popular combination!*)
   88.40 -fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;
   88.41 +fun ares_tac rules = atac  ORELSE'  resolve_tac rules;
   88.42  
   88.43 -fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   88.44 +fun solve_tac rules = resolve_tac rules THEN_ALL_NEW atac;
   88.45  
   88.46  (*Matching tactics -- as above, but forbid updating of state*)
   88.47  fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i);
    89.1 --- a/src/Sequents/simpdata.ML	Sun Nov 09 20:49:28 2014 +0100
    89.2 +++ b/src/Sequents/simpdata.ML	Mon Nov 10 21:49:48 2014 +0100
    89.3 @@ -58,7 +58,7 @@
    89.4    @{thm iff_refl}, reflexive_thm];
    89.5  
    89.6  fun unsafe_solver ctxt =
    89.7 -  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac];
    89.8 +  FIRST' [resolve_tac (triv_rls @ Simplifier.prems_of ctxt), assume_tac ctxt];
    89.9  
   89.10  (*No premature instantiation of variables during simplification*)
   89.11  fun safe_solver ctxt =
    90.1 --- a/src/Tools/intuitionistic.ML	Sun Nov 09 20:49:28 2014 +0100
    90.2 +++ b/src/Tools/intuitionistic.ML	Mon Nov 10 21:49:48 2014 +0100
    90.3 @@ -34,7 +34,7 @@
    90.4  
    90.5  fun unsafe_step_tac ctxt =
    90.6    Context_Rules.wrap ctxt
    90.7 -   (assume_tac APPEND'
    90.8 +   (assume_tac ctxt APPEND'
    90.9      bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
   90.10      bires_tac false (Context_Rules.netpair ctxt));
   90.11  
    91.1 --- a/src/ZF/Tools/inductive_package.ML	Sun Nov 09 20:49:28 2014 +0100
    91.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 10 21:49:48 2014 +0100
    91.3 @@ -220,7 +220,7 @@
    91.4       resolve_tac [disjIn] 2,
    91.5       (*Not ares_tac, since refl must be tried before equality assumptions;
    91.6         backtracking may occur if the premises have extra variables!*)
    91.7 -     DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
    91.8 +     DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac ctxt 2),
    91.9       (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
   91.10       rewrite_goals_tac ctxt con_defs,
   91.11       REPEAT (resolve_tac @{thms refl} 2),
   91.12 @@ -233,7 +233,7 @@
   91.13                          ORELSE' hyp_subst_tac ctxt1)),
   91.14       if !Ind_Syntax.trace then print_tac ctxt "The subgoal after monos, type_elims:"
   91.15       else all_tac,
   91.16 -     DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
   91.17 +     DEPTH_SOLVE (swap_res_tac ctxt (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
   91.18  
   91.19    (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
   91.20    val mk_disj_rls = Balanced_Tree.accesses
   91.21 @@ -330,7 +330,7 @@
   91.22               |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
   91.23             setSolver (mk_solver "minimal"
   91.24                        (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)
   91.25 -                                   ORELSE' assume_tac
   91.26 +                                   ORELSE' assume_tac ctxt
   91.27                                     ORELSE' eresolve_tac @{thms FalseE}));
   91.28  
   91.29       val quant_induct =
    92.1 --- a/src/ZF/Tools/typechk.ML	Sun Nov 09 20:49:28 2014 +0100
    92.2 +++ b/src/ZF/Tools/typechk.ML	Mon Nov 10 21:49:48 2014 +0100
    92.3 @@ -81,16 +81,17 @@
    92.4    | is_rigid_elem _ = false;
    92.5  
    92.6  (*Try solving a:A by assumption provided a is rigid!*)
    92.7 -val test_assume_tac = SUBGOAL(fn (prem,i) =>
    92.8 +fun test_assume_tac ctxt = SUBGOAL(fn (prem,i) =>
    92.9      if is_rigid_elem (Logic.strip_assums_concl prem)
   92.10 -    then  assume_tac i  else  eq_assume_tac i);
   92.11 +    then  assume_tac ctxt i  else  eq_assume_tac i);
   92.12  
   92.13  (*Type checking solves a:?A (a rigid, ?A maybe flexible).
   92.14    match_tac is too strict; would refuse to instantiate ?A*)
   92.15 -fun typecheck_step_tac (TC{net,...}) =
   92.16 -    FIRSTGOAL (test_assume_tac ORELSE' net_res_tac 3 net);
   92.17 +fun typecheck_step_tac ctxt =
   92.18 +  let val TC {net, ...} = tcset_of ctxt
   92.19 +  in FIRSTGOAL (test_assume_tac ctxt ORELSE' net_res_tac 3 net) end;
   92.20  
   92.21 -fun typecheck_tac ctxt = REPEAT (typecheck_step_tac (tcset_of ctxt));
   92.22 +fun typecheck_tac ctxt = REPEAT (typecheck_step_tac ctxt);
   92.23  
   92.24  (*Compiles a term-net for speed*)
   92.25  val basic_res_tac = net_resolve_tac [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl},
   92.26 @@ -102,7 +103,7 @@
   92.27      (DEPTH_SOLVE (eresolve_tac @{thms FalseE} 1
   92.28                    ORELSE basic_res_tac 1
   92.29                    ORELSE (ares_tac hyps 1
   92.30 -                          APPEND typecheck_step_tac (tcset_of ctxt))));
   92.31 +                          APPEND typecheck_step_tac ctxt)));
   92.32  
   92.33  val type_solver =
   92.34    Simplifier.mk_solver "ZF typecheck" (fn ctxt =>
    93.1 --- a/src/ZF/UNITY/Constrains.thy	Sun Nov 09 20:49:28 2014 +0100
    93.2 +++ b/src/ZF/UNITY/Constrains.thy	Mon Nov 10 21:49:48 2014 +0100
    93.3 @@ -459,7 +459,8 @@
    93.4  ML
    93.5  {*
    93.6  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
    93.7 -val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin};
    93.8 +fun Always_Int_tac ctxt =
    93.9 +  dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin};
   93.10  
   93.11  (*Combines a list of invariance THEOREMS into one.*)
   93.12  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
   93.13 @@ -468,7 +469,7 @@
   93.14  
   93.15  fun constrains_tac ctxt =
   93.16     SELECT_GOAL
   93.17 -      (EVERY [REPEAT (Always_Int_tac 1),
   93.18 +      (EVERY [REPEAT (Always_Int_tac ctxt 1),
   93.19                REPEAT (etac @{thm Always_ConstrainsI} 1
   93.20                        ORELSE
   93.21                        resolve_tac [@{thm StableI}, @{thm stableI},
    94.1 --- a/src/ZF/UNITY/SubstAx.thy	Sun Nov 09 20:49:28 2014 +0100
    94.2 +++ b/src/ZF/UNITY/SubstAx.thy	Mon Nov 10 21:49:48 2014 +0100
    94.3 @@ -352,7 +352,7 @@
    94.4  (*proves "ensures/leadsTo" properties when the program is specified*)
    94.5  fun ensures_tac ctxt sact =
    94.6    SELECT_GOAL
    94.7 -    (EVERY [REPEAT (Always_Int_tac 1),
    94.8 +    (EVERY [REPEAT (Always_Int_tac ctxt 1),
    94.9              etac @{thm Always_LeadsTo_Basis} 1
   94.10                  ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   94.11                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},