proper context for match_tac etc.;
authorwenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957c9e744ea8a38
parent 58956 a816aa3ff391
child 58958 114255dce178
proper context for match_tac etc.;
NEWS
src/CCL/Wfd.thy
src/Doc/Implementation/Tactic.thy
src/FOL/FOL.thy
src/FOL/intprover.ML
src/FOL/simpdata.ML
src/FOLP/FOLP.thy
src/FOLP/classical.ML
src/FOLP/ex/Classical.thy
src/FOLP/ex/If.thy
src/FOLP/ex/Intro.thy
src/FOLP/ex/Propositional_Cla.thy
src/FOLP/ex/Quantifiers_Cla.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/IOA/meta_theory/Automata.thy
src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/NSA/transfer.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/SMT/z3_replay_methods.ML
src/HOL/Tools/simpdata.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/hypsubst.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/method.ML
src/Pure/simplifier.ML
src/Pure/tactic.ML
src/Sequents/simpdata.ML
src/Tools/induct.ML
src/Tools/intuitionistic.ML
     1.1 --- a/NEWS	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/NEWS	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 -* Proper context for various elementary tactics: compose_tac,
     1.8 +* Proper context for various elementary tactics: match_tac, compose_tac,
     1.9  Splitter.split_tac etc.  Minor INCOMPATIBILITY.
    1.10  
    1.11  * Tactical PARALLEL_ALLGOALS is the most common way to refer to
     2.1 --- a/src/CCL/Wfd.thy	Sun Nov 09 14:08:00 2014 +0100
     2.2 +++ b/src/CCL/Wfd.thy	Sun Nov 09 17:04:14 2014 +0100
     2.3 @@ -453,10 +453,11 @@
     2.4    in IHinst tac @{thms rcallTs} i end
     2.5    THEN eresolve_tac @{thms rcall_lemmas} i
     2.6  
     2.7 -fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE
     2.8 -                           rcall_tac ctxt i ORELSE
     2.9 -                           ematch_tac [@{thm SubtypeE}] i ORELSE
    2.10 -                           match_tac [@{thm SubtypeI}] i
    2.11 +fun raw_step_tac ctxt prems i =
    2.12 +  ares_tac (prems@type_rls) i ORELSE
    2.13 +  rcall_tac ctxt i ORELSE
    2.14 +  ematch_tac ctxt [@{thm SubtypeE}] i ORELSE
    2.15 +  match_tac ctxt [@{thm SubtypeI}] i
    2.16  
    2.17  fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
    2.18            if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
     3.1 --- a/src/Doc/Implementation/Tactic.thy	Sun Nov 09 14:08:00 2014 +0100
     3.2 +++ b/src/Doc/Implementation/Tactic.thy	Sun Nov 09 17:04:14 2014 +0100
     3.3 @@ -284,10 +284,10 @@
     3.4    @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
     3.5    @{index_ML assume_tac: "int -> tactic"} \\
     3.6    @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
     3.7 -  @{index_ML match_tac: "thm list -> int -> tactic"} \\
     3.8 -  @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
     3.9 -  @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
    3.10 -  @{index_ML bimatch_tac: "(bool * thm) list -> int -> tactic"} \\
    3.11 +  @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
    3.12 +  @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
    3.13 +  @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
    3.14 +  @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
    3.15    \end{mldecls}
    3.16  
    3.17    \begin{description}
     4.1 --- a/src/FOL/FOL.thy	Sun Nov 09 14:08:00 2014 +0100
     4.2 +++ b/src/FOL/FOL.thy	Sun Nov 09 17:04:14 2014 +0100
     4.3 @@ -420,7 +420,7 @@
     4.4      val rulify_fallback = @{thms induct_rulify_fallback}
     4.5      val equal_def = @{thm induct_equal_def}
     4.6      fun dest_def _ = NONE
     4.7 -    fun trivial_tac _ = no_tac
     4.8 +    fun trivial_tac _ _ = no_tac
     4.9    );
    4.10  *}
    4.11  
     5.1 --- a/src/FOL/intprover.ML	Sun Nov 09 14:08:00 2014 +0100
     5.2 +++ b/src/FOL/intprover.ML	Sun Nov 09 17:04:14 2014 +0100
     5.3 @@ -66,9 +66,9 @@
     5.4    FIRST' [
     5.5      eq_assume_tac,
     5.6      eq_mp_tac,
     5.7 -    bimatch_tac safe0_brls,
     5.8 +    bimatch_tac ctxt safe0_brls,
     5.9      hyp_subst_tac ctxt,
    5.10 -    bimatch_tac safep_brls];
    5.11 +    bimatch_tac ctxt safep_brls];
    5.12  
    5.13  (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
    5.14  fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
     6.1 --- a/src/FOL/simpdata.ML	Sun Nov 09 14:08:00 2014 +0100
     6.2 +++ b/src/FOL/simpdata.ML	Sun Nov 09 17:04:14 2014 +0100
     6.3 @@ -113,7 +113,8 @@
     6.4  
     6.5  (*No premature instantiation of variables during simplification*)
     6.6  fun safe_solver ctxt =
     6.7 -  FIRST' [match_tac (triv_rls @ Simplifier.prems_of ctxt), eq_assume_tac, ematch_tac @{thms FalseE}];
     6.8 +  FIRST' [match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt),
     6.9 +    eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
    6.10  
    6.11  (*No simprules, but basic infastructure for simplification*)
    6.12  val FOL_basic_ss =
     7.1 --- a/src/FOLP/FOLP.thy	Sun Nov 09 14:08:00 2014 +0100
     7.2 +++ b/src/FOLP/FOLP.thy	Sun Nov 09 17:04:14 2014 +0100
     7.3 @@ -134,7 +134,7 @@
     7.4    "?p2 : ~P | P"
     7.5    "?p3 : ~ ~ P <-> P"
     7.6    "?p4 : (~P --> P) <-> P"
     7.7 -  apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})
     7.8 +  apply (tactic {* ALLGOALS (Cla.fast_tac @{context} FOLP_cs) *})
     7.9    done
    7.10  
    7.11  ML_file "simpdata.ML"
     8.1 --- a/src/FOLP/classical.ML	Sun Nov 09 14:08:00 2014 +0100
     8.2 +++ b/src/FOLP/classical.ML	Sun Nov 09 17:04:14 2014 +0100
     8.3 @@ -44,19 +44,19 @@
     8.4        {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
     8.5         safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
     8.6         haz_brls: (bool*thm)list}
     8.7 -  val best_tac : claset -> int -> tactic
     8.8 +  val best_tac : Proof.context -> claset -> int -> tactic
     8.9    val contr_tac : int -> tactic
    8.10 -  val fast_tac : claset -> int -> tactic
    8.11 +  val fast_tac : Proof.context -> claset -> int -> tactic
    8.12    val inst_step_tac : int -> tactic
    8.13    val joinrules : thm list * thm list -> (bool * thm) list
    8.14    val mp_tac: int -> tactic
    8.15 -  val safe_tac : claset -> tactic
    8.16 -  val safe_step_tac : claset -> int -> tactic
    8.17 -  val slow_step_tac : claset -> int -> tactic
    8.18 -  val step_tac : claset -> int -> tactic
    8.19 +  val safe_tac : Proof.context -> claset -> tactic
    8.20 +  val safe_step_tac : Proof.context -> claset -> int -> tactic
    8.21 +  val slow_step_tac : Proof.context -> claset -> int -> tactic
    8.22 +  val step_tac : Proof.context -> claset -> int -> tactic
    8.23    val swapify : thm list -> thm list
    8.24    val swap_res_tac : thm list -> int -> tactic
    8.25 -  val uniq_mp_tac: int -> tactic
    8.26 +  val uniq_mp_tac: Proof.context -> int -> tactic
    8.27    end;
    8.28  
    8.29  
    8.30 @@ -76,7 +76,7 @@
    8.31  fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
    8.32  
    8.33  (*Like mp_tac but instantiates no variables*)
    8.34 -fun uniq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
    8.35 +fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
    8.36  
    8.37  (*Creates rules to eliminate ~A, from rules to introduce A*)
    8.38  fun swapify intrs = intrs RLN (2, [swap]);
    8.39 @@ -148,38 +148,38 @@
    8.40  (*** Simple tactics for theorem proving ***)
    8.41  
    8.42  (*Attack subgoals using safe inferences*)
    8.43 -fun safe_step_tac (CS{safe0_brls,safep_brls,...}) = 
    8.44 +fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 
    8.45    FIRST' [uniq_assume_tac,
    8.46 -          uniq_mp_tac,
    8.47 +          uniq_mp_tac ctxt,
    8.48            biresolve_tac safe0_brls,
    8.49            FIRST' hyp_subst_tacs,
    8.50            biresolve_tac safep_brls] ;
    8.51  
    8.52  (*Repeatedly attack subgoals using safe inferences*)
    8.53 -fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));
    8.54 +fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
    8.55  
    8.56  (*These steps could instantiate variables and are therefore unsafe.*)
    8.57  val inst_step_tac = assume_tac APPEND' contr_tac;
    8.58  
    8.59  (*Single step for the prover.  FAILS unless it makes progress. *)
    8.60 -fun step_tac (cs as (CS{haz_brls,...})) i = 
    8.61 -  FIRST [safe_tac cs,
    8.62 +fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 
    8.63 +  FIRST [safe_tac ctxt cs,
    8.64           inst_step_tac i,
    8.65           biresolve_tac haz_brls i];
    8.66  
    8.67  (*** The following tactics all fail unless they solve one goal ***)
    8.68  
    8.69  (*Dumb but fast*)
    8.70 -fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
    8.71 +fun fast_tac ctxt cs = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt cs 1));
    8.72  
    8.73  (*Slower but smarter than fast_tac*)
    8.74 -fun best_tac cs = 
    8.75 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
    8.76 +fun best_tac ctxt cs = 
    8.77 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1));
    8.78  
    8.79  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
    8.80    allows backtracking from "safe" rules to "unsafe" rules here.*)
    8.81 -fun slow_step_tac (cs as (CS{haz_brls,...})) i = 
    8.82 -    safe_tac cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
    8.83 +fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 
    8.84 +    safe_tac ctxt cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
    8.85  
    8.86  end; 
    8.87  end;
     9.1 --- a/src/FOLP/ex/Classical.thy	Sun Nov 09 14:08:00 2014 +0100
     9.2 +++ b/src/FOLP/ex/Classical.thy	Sun Nov 09 17:04:14 2014 +0100
     9.3 @@ -10,14 +10,14 @@
     9.4  begin
     9.5  
     9.6  schematic_lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
     9.7 -  by (tactic "fast_tac FOLP_cs 1")
     9.8 +  by (tactic "fast_tac @{context} FOLP_cs 1")
     9.9  
    9.10  (*If and only if*)
    9.11  schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
    9.12 -  by (tactic "fast_tac FOLP_cs 1")
    9.13 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.14  
    9.15  schematic_lemma "?p : ~ (P <-> ~P)"
    9.16 -  by (tactic "fast_tac FOLP_cs 1")
    9.17 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.18  
    9.19  
    9.20  (*Sample problems from 
    9.21 @@ -33,134 +33,134 @@
    9.22  text "Pelletier's examples"
    9.23  (*1*)
    9.24  schematic_lemma "?p : (P-->Q)  <->  (~Q --> ~P)"
    9.25 -  by (tactic "fast_tac FOLP_cs 1")
    9.26 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.27  
    9.28  (*2*)
    9.29  schematic_lemma "?p : ~ ~ P  <->  P"
    9.30 -  by (tactic "fast_tac FOLP_cs 1")
    9.31 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.32  
    9.33  (*3*)
    9.34  schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
    9.35 -  by (tactic "fast_tac FOLP_cs 1")
    9.36 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.37  
    9.38  (*4*)
    9.39  schematic_lemma "?p : (~P-->Q)  <->  (~Q --> P)"
    9.40 -  by (tactic "fast_tac FOLP_cs 1")
    9.41 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.42  
    9.43  (*5*)
    9.44  schematic_lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
    9.45 -  by (tactic "fast_tac FOLP_cs 1")
    9.46 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.47  
    9.48  (*6*)
    9.49  schematic_lemma "?p : P | ~ P"
    9.50 -  by (tactic "fast_tac FOLP_cs 1")
    9.51 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.52  
    9.53  (*7*)
    9.54  schematic_lemma "?p : P | ~ ~ ~ P"
    9.55 -  by (tactic "fast_tac FOLP_cs 1")
    9.56 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.57  
    9.58  (*8.  Peirce's law*)
    9.59  schematic_lemma "?p : ((P-->Q) --> P)  -->  P"
    9.60 -  by (tactic "fast_tac FOLP_cs 1")
    9.61 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.62  
    9.63  (*9*)
    9.64  schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
    9.65 -  by (tactic "fast_tac FOLP_cs 1")
    9.66 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.67  
    9.68  (*10*)
    9.69  schematic_lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
    9.70 -  by (tactic "fast_tac FOLP_cs 1")
    9.71 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.72  
    9.73  (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
    9.74  schematic_lemma "?p : P<->P"
    9.75 -  by (tactic "fast_tac FOLP_cs 1")
    9.76 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.77  
    9.78  (*12.  "Dijkstra's law"*)
    9.79  schematic_lemma "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
    9.80 -  by (tactic "fast_tac FOLP_cs 1")
    9.81 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.82  
    9.83  (*13.  Distributive law*)
    9.84  schematic_lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
    9.85 -  by (tactic "fast_tac FOLP_cs 1")
    9.86 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.87  
    9.88  (*14*)
    9.89  schematic_lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
    9.90 -  by (tactic "fast_tac FOLP_cs 1")
    9.91 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.92  
    9.93  (*15*)
    9.94  schematic_lemma "?p : (P --> Q) <-> (~P | Q)"
    9.95 -  by (tactic "fast_tac FOLP_cs 1")
    9.96 +  by (tactic "fast_tac @{context} FOLP_cs 1")
    9.97  
    9.98  (*16*)
    9.99  schematic_lemma "?p : (P-->Q) | (Q-->P)"
   9.100 -  by (tactic "fast_tac FOLP_cs 1")
   9.101 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.102  
   9.103  (*17*)
   9.104  schematic_lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
   9.105 -  by (tactic "fast_tac FOLP_cs 1")
   9.106 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.107  
   9.108  
   9.109  text "Classical Logic: examples with quantifiers"
   9.110  
   9.111  schematic_lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
   9.112 -  by (tactic "fast_tac FOLP_cs 1")
   9.113 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.114  
   9.115  schematic_lemma "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
   9.116 -  by (tactic "fast_tac FOLP_cs 1")
   9.117 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.118  
   9.119  schematic_lemma "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
   9.120 -  by (tactic "fast_tac FOLP_cs 1")
   9.121 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.122  
   9.123  schematic_lemma "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
   9.124 -  by (tactic "fast_tac FOLP_cs 1")
   9.125 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.126  
   9.127  
   9.128  text "Problems requiring quantifier duplication"
   9.129  
   9.130  (*Needs multiple instantiation of ALL.*)
   9.131  schematic_lemma "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
   9.132 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.133 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.134  
   9.135  (*Needs double instantiation of the quantifier*)
   9.136  schematic_lemma "?p : EX x. P(x) --> P(a) & P(b)"
   9.137 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.138 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.139  
   9.140  schematic_lemma "?p : EX z. P(z) --> (ALL x. P(x))"
   9.141 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.142 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.143  
   9.144  
   9.145  text "Hard examples with quantifiers"
   9.146  
   9.147  text "Problem 18"
   9.148  schematic_lemma "?p : EX y. ALL x. P(y)-->P(x)"
   9.149 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.150 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.151  
   9.152  text "Problem 19"
   9.153  schematic_lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
   9.154 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.155 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.156  
   9.157  text "Problem 20"
   9.158  schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
   9.159      --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
   9.160 -  by (tactic "fast_tac FOLP_cs 1")
   9.161 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.162  
   9.163  text "Problem 21"
   9.164  schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
   9.165 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.166 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.167  
   9.168  text "Problem 22"
   9.169  schematic_lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
   9.170 -  by (tactic "fast_tac FOLP_cs 1")
   9.171 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.172  
   9.173  text "Problem 23"
   9.174  schematic_lemma "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
   9.175 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.176 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.177  
   9.178  text "Problem 24"
   9.179  schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
   9.180       (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
   9.181      --> (EX x. P(x)&R(x))"
   9.182 -  by (tactic "fast_tac FOLP_cs 1")
   9.183 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.184  
   9.185  text "Problem 25"
   9.186  schematic_lemma "?p : (EX x. P(x)) &  
   9.187 @@ -174,7 +174,7 @@
   9.188  schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
   9.189       (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   
   9.190    --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
   9.191 -  by (tactic "fast_tac FOLP_cs 1")
   9.192 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.193  
   9.194  text "Problem 27"
   9.195  schematic_lemma "?p : (EX x. P(x) & ~Q(x)) &    
   9.196 @@ -182,49 +182,49 @@
   9.197                (ALL x. M(x) & L(x) --> P(x)) &    
   9.198                ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))   
   9.199            --> (ALL x. M(x) --> ~L(x))"
   9.200 -  by (tactic "fast_tac FOLP_cs 1")
   9.201 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.202  
   9.203  text "Problem 28.  AMENDED"
   9.204  schematic_lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &    
   9.205          ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &   
   9.206          ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))   
   9.207      --> (ALL x. P(x) & L(x) --> M(x))"
   9.208 -  by (tactic "fast_tac FOLP_cs 1")
   9.209 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.210  
   9.211  text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
   9.212  schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
   9.213      --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
   9.214           (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
   9.215 -  by (tactic "fast_tac FOLP_cs 1")
   9.216 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.217  
   9.218  text "Problem 30"
   9.219  schematic_lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &  
   9.220          (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
   9.221      --> (ALL x. S(x))"
   9.222 -  by (tactic "fast_tac FOLP_cs 1")
   9.223 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.224  
   9.225  text "Problem 31"
   9.226  schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
   9.227          (EX x. L(x) & P(x)) &  
   9.228          (ALL x. ~ R(x) --> M(x))   
   9.229      --> (EX x. L(x) & M(x))"
   9.230 -  by (tactic "fast_tac FOLP_cs 1")
   9.231 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.232  
   9.233  text "Problem 32"
   9.234  schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
   9.235          (ALL x. S(x) & R(x) --> L(x)) &  
   9.236          (ALL x. M(x) --> R(x))   
   9.237      --> (ALL x. P(x) & M(x) --> L(x))"
   9.238 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.239 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.240  
   9.241  text "Problem 33"
   9.242  schematic_lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->     
   9.243       (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
   9.244 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.245 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.246  
   9.247  text "Problem 35"
   9.248  schematic_lemma "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))"
   9.249 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.250 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.251  
   9.252  text "Problem 36"
   9.253  schematic_lemma
   9.254 @@ -232,7 +232,7 @@
   9.255        (ALL x. EX y. G(x,y)) &  
   9.256        (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))    
   9.257    --> (ALL x. EX y. H(x,y))"
   9.258 -  by (tactic "fast_tac FOLP_cs 1")
   9.259 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.260  
   9.261  text "Problem 37"
   9.262  schematic_lemma "?p : (ALL z. EX w. ALL x. EX y.  
   9.263 @@ -240,63 +240,63 @@
   9.264          (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &  
   9.265          ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))   
   9.266      --> (ALL x. EX y. R(x,y))"
   9.267 -  by (tactic "fast_tac FOLP_cs 1")
   9.268 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.269  
   9.270  text "Problem 39"
   9.271  schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
   9.272 -  by (tactic "fast_tac FOLP_cs 1")
   9.273 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.274  
   9.275  text "Problem 40.  AMENDED"
   9.276  schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
   9.277                ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
   9.278 -  by (tactic "fast_tac FOLP_cs 1")
   9.279 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.280  
   9.281  text "Problem 41"
   9.282  schematic_lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))   
   9.283            --> ~ (EX z. ALL x. f(x,z))"
   9.284 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.285 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.286  
   9.287  text "Problem 44"
   9.288  schematic_lemma "?p : (ALL x. f(x) -->                                     
   9.289                (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
   9.290                (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
   9.291                --> (EX x. j(x) & ~f(x))"
   9.292 -  by (tactic "fast_tac FOLP_cs 1")
   9.293 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.294  
   9.295  text "Problems (mainly) involving equality or functions"
   9.296  
   9.297  text "Problem 48"
   9.298  schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
   9.299 -  by (tactic "fast_tac FOLP_cs 1")
   9.300 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.301  
   9.302  text "Problem 50"
   9.303  (*What has this to do with equality?*)
   9.304  schematic_lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
   9.305 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.306 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.307  
   9.308  text "Problem 56"
   9.309  schematic_lemma
   9.310   "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
   9.311 -  by (tactic "fast_tac FOLP_cs 1")
   9.312 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.313  
   9.314  text "Problem 57"
   9.315  schematic_lemma
   9.316  "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
   9.317        (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
   9.318 -  by (tactic "fast_tac FOLP_cs 1")
   9.319 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.320  
   9.321  text "Problem 58  NOT PROVED AUTOMATICALLY"
   9.322  schematic_lemma
   9.323    notes f_cong = subst_context [where t = f]
   9.324    shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
   9.325 -  by (tactic {* fast_tac (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
   9.326 +  by (tactic {* fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
   9.327  
   9.328  text "Problem 59"
   9.329  schematic_lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
   9.330 -  by (tactic "best_tac FOLP_dup_cs 1")
   9.331 +  by (tactic "best_tac @{context} FOLP_dup_cs 1")
   9.332  
   9.333  text "Problem 60"
   9.334  schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
   9.335 -  by (tactic "fast_tac FOLP_cs 1")
   9.336 +  by (tactic "fast_tac @{context} FOLP_cs 1")
   9.337  
   9.338  end
    10.1 --- a/src/FOLP/ex/If.thy	Sun Nov 09 14:08:00 2014 +0100
    10.2 +++ b/src/FOLP/ex/If.thy	Sun Nov 09 17:04:14 2014 +0100
    10.3 @@ -9,7 +9,7 @@
    10.4    assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
    10.5    shows "?p : if(P,Q,R)"
    10.6  apply (unfold if_def)
    10.7 -apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
    10.8 +apply (tactic {* fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1 *})
    10.9  done
   10.10  
   10.11  schematic_lemma ifE:
   10.12 @@ -19,7 +19,7 @@
   10.13    shows "?p : S"
   10.14  apply (insert 1)
   10.15  apply (unfold if_def)
   10.16 -apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
   10.17 +apply (tactic {* fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
   10.18  done
   10.19  
   10.20  schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
   10.21 @@ -33,11 +33,11 @@
   10.22  ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
   10.23  
   10.24  schematic_lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
   10.25 -apply (tactic {* fast_tac if_cs 1 *})
   10.26 +apply (tactic {* fast_tac @{context} if_cs 1 *})
   10.27  done
   10.28  
   10.29  schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
   10.30 -apply (tactic {* fast_tac if_cs 1 *})
   10.31 +apply (tactic {* fast_tac @{context} if_cs 1 *})
   10.32  done
   10.33  
   10.34  end
    11.1 --- a/src/FOLP/ex/Intro.thy	Sun Nov 09 14:08:00 2014 +0100
    11.2 +++ b/src/FOLP/ex/Intro.thy	Sun Nov 09 17:04:14 2014 +0100
    11.3 @@ -45,13 +45,13 @@
    11.4  
    11.5  schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
    11.6          -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
    11.7 -apply (tactic {* fast_tac FOLP_cs 1 *})
    11.8 +apply (tactic {* fast_tac @{context} FOLP_cs 1 *})
    11.9  done
   11.10  
   11.11  
   11.12  schematic_lemma "?p : ALL x. P(x,f(x)) <->
   11.13          (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
   11.14 -apply (tactic {* fast_tac FOLP_cs 1 *})
   11.15 +apply (tactic {* fast_tac @{context} FOLP_cs 1 *})
   11.16  done
   11.17  
   11.18  
    12.1 --- a/src/FOLP/ex/Propositional_Cla.thy	Sun Nov 09 14:08:00 2014 +0100
    12.2 +++ b/src/FOLP/ex/Propositional_Cla.thy	Sun Nov 09 17:04:14 2014 +0100
    12.3 @@ -12,106 +12,106 @@
    12.4  
    12.5  text "commutative laws of & and | "
    12.6  schematic_lemma "?p : P & Q  -->  Q & P"
    12.7 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    12.8 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    12.9  
   12.10  schematic_lemma "?p : P | Q  -->  Q | P"
   12.11 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.12 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.13  
   12.14  
   12.15  text "associative laws of & and | "
   12.16  schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
   12.17 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.18 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.19  
   12.20  schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
   12.21 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.22 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.23  
   12.24  
   12.25  text "distributive laws of & and | "
   12.26  schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
   12.27 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.28 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.29  
   12.30  schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
   12.31 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.32 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.33  
   12.34  schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
   12.35 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.36 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.37  
   12.38  
   12.39  schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
   12.40 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.41 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.42  
   12.43  
   12.44  text "Laws involving implication"
   12.45  
   12.46  schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
   12.47 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.48 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.49  
   12.50  schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
   12.51 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.52 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.53  
   12.54  schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
   12.55 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.56 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.57  
   12.58  schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
   12.59 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.60 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.61  
   12.62  schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
   12.63 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.64 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.65  
   12.66  
   12.67  text "Propositions-as-types"
   12.68  
   12.69  (*The combinator K*)
   12.70  schematic_lemma "?p : P --> (Q --> P)"
   12.71 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.72 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.73  
   12.74  (*The combinator S*)
   12.75  schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
   12.76 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.77 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.78  
   12.79  
   12.80  (*Converse is classical*)
   12.81  schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
   12.82 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.83 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.84  
   12.85  schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
   12.86 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.87 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.88  
   12.89  
   12.90  text "Schwichtenberg's examples (via T. Nipkow)"
   12.91  
   12.92  schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
   12.93 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.94 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   12.95  
   12.96  schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
   12.97                --> ((P --> Q) --> P) --> P"
   12.98 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   12.99 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  12.100  
  12.101  schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
  12.102                 --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
  12.103 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  12.104 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  12.105    
  12.106  schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
  12.107 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  12.108 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  12.109  
  12.110  schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
  12.111 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  12.112 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  12.113  
  12.114  schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
  12.115 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  12.116 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  12.117  
  12.118  schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
  12.119            --> (((P8 --> P2) --> P9) --> P3 --> P10)  
  12.120            --> (P1 --> P8) --> P6 --> P7  
  12.121            --> (((P3 --> P2) --> P9) --> P4)  
  12.122            --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
  12.123 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  12.124 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  12.125  
  12.126  schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
  12.127       --> (((P3 --> P2) --> P9) --> P4)  
  12.128       --> (((P6 --> P1) --> P2) --> P9)  
  12.129       --> (((P7 --> P1) --> P10) --> P4 --> P5)  
  12.130       --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
  12.131 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  12.132 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  12.133  
  12.134  end
    13.1 --- a/src/FOLP/ex/Quantifiers_Cla.thy	Sun Nov 09 14:08:00 2014 +0100
    13.2 +++ b/src/FOLP/ex/Quantifiers_Cla.thy	Sun Nov 09 17:04:14 2014 +0100
    13.3 @@ -11,91 +11,91 @@
    13.4  begin
    13.5  
    13.6  schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
    13.7 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
    13.8 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
    13.9  
   13.10  schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
   13.11 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.12 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.13  
   13.14  
   13.15  (*Converse is false*)
   13.16  schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
   13.17 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.18 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.19  
   13.20  schematic_lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
   13.21 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.22 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.23  
   13.24  
   13.25  schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
   13.26 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.27 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.28  
   13.29  
   13.30  text "Some harder ones"
   13.31  
   13.32  schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
   13.33 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.34 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.35  
   13.36  (*Converse is false*)
   13.37  schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
   13.38 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.39 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.40  
   13.41  
   13.42  text "Basic test of quantifier reasoning"
   13.43  (*TRUE*)
   13.44  schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   13.45 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.46 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.47  
   13.48  schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   13.49 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.50 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.51  
   13.52  
   13.53  text "The following should fail, as they are false!"
   13.54  
   13.55  schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
   13.56 -  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
   13.57 +  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
   13.58    oops
   13.59  
   13.60  schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
   13.61 -  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
   13.62 +  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
   13.63    oops
   13.64  
   13.65  schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
   13.66 -  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
   13.67 +  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
   13.68    oops
   13.69  
   13.70  schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
   13.71 -  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
   13.72 +  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
   13.73    oops
   13.74  
   13.75  
   13.76  text "Back to things that are provable..."
   13.77  
   13.78  schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
   13.79 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.80 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.81  
   13.82  
   13.83  (*An example of why exI should be delayed as long as possible*)
   13.84  schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
   13.85 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.86 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.87  
   13.88  schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
   13.89 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.90 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.91  
   13.92  schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
   13.93 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
   13.94 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   13.95  
   13.96  
   13.97  text "Some slow ones"
   13.98  
   13.99  (*Principia Mathematica *11.53  *)
  13.100  schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
  13.101 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  13.102 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  13.103  
  13.104  (*Principia Mathematica *11.55  *)
  13.105  schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
  13.106 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  13.107 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  13.108  
  13.109  (*Principia Mathematica *11.61  *)
  13.110  schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
  13.111 -  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
  13.112 +  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
  13.113  
  13.114  end
    14.1 --- a/src/HOL/HOL.thy	Sun Nov 09 14:08:00 2014 +0100
    14.2 +++ b/src/HOL/HOL.thy	Sun Nov 09 17:04:14 2014 +0100
    14.3 @@ -1463,7 +1463,7 @@
    14.4    val equal_def = @{thm induct_equal_def}
    14.5    fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
    14.6      | dest_def _ = NONE
    14.7 -  val trivial_tac = match_tac @{thms induct_trueI}
    14.8 +  fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
    14.9  )
   14.10  *}
   14.11  
    15.1 --- a/src/HOL/HOLCF/Cfun.thy	Sun Nov 09 14:08:00 2014 +0100
    15.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sun Nov 09 17:04:14 2014 +0100
    15.3 @@ -148,7 +148,7 @@
    15.4        val tr = instantiate' [SOME T, SOME U] [SOME f]
    15.5            (mk_meta_eq @{thm Abs_cfun_inverse2});
    15.6        val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
    15.7 -      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)));
    15.8 +      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
    15.9      in SOME (perhaps (SINGLE (tac 1)) tr) end
   15.10  *}
   15.11  
    16.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 09 14:08:00 2014 +0100
    16.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 09 17:04:14 2014 +0100
    16.3 @@ -391,7 +391,6 @@
    16.4  
    16.5  subsection "input_enabledness and par"
    16.6  
    16.7 -
    16.8  (* ugly case distinctions. Heart of proof:
    16.9       1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
   16.10       2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
   16.11 @@ -400,7 +399,7 @@
   16.12        ==> input_enabled (A||B)"
   16.13  apply (unfold input_enabled_def)
   16.14  apply (simp add: Let_def inputs_of_par trans_of_par)
   16.15 -apply (tactic "safe_tac @{theory_context Fun}")
   16.16 +apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
   16.17  apply (simp add: inp_is_act)
   16.18  prefer 2
   16.19  apply (simp add: inp_is_act)
    17.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 09 14:08:00 2014 +0100
    17.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 09 17:04:14 2014 +0100
    17.3 @@ -297,7 +297,8 @@
    17.4  fun mkex_induct_tac ctxt sch exA exB =
    17.5    EVERY'[Seq_induct_tac ctxt sch defs,
    17.6           asm_full_simp_tac ctxt,
    17.7 -         SELECT_GOAL (safe_tac @{theory_context Fun}),
    17.8 +         SELECT_GOAL
    17.9 +          (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
   17.10           Seq_case_simp_tac ctxt exA,
   17.11           Seq_case_simp_tac ctxt exB,
   17.12           asm_full_simp_tac ctxt,
    18.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 09 14:08:00 2014 +0100
    18.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 09 17:04:14 2014 +0100
    18.3 @@ -151,9 +151,9 @@
    18.4        let
    18.5          val prop = mk_trp (mk_cont functional)
    18.6          val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
    18.7 -        val tac = REPEAT_ALL_NEW (match_tac (rev rules)) 1
    18.8 +        fun tac ctxt = REPEAT_ALL_NEW (match_tac ctxt (rev rules)) 1
    18.9        in
   18.10 -        Goal.prove_global thy [] [] prop (K tac)
   18.11 +        Goal.prove_global thy [] [] prop (tac o #context)
   18.12        end
   18.13  
   18.14      val tuple_unfold_thm =
    19.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun Nov 09 14:08:00 2014 +0100
    19.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sun Nov 09 17:04:14 2014 +0100
    19.3 @@ -131,7 +131,7 @@
    19.4            "The error occurred for the goal statement:\n" ^
    19.5            Syntax.string_of_term lthy prop)
    19.6          val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
    19.7 -        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)))
    19.8 +        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac lthy (rev rules)))
    19.9          val slow_tac = SOLVED' (simp_tac lthy)
   19.10          val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
   19.11        in
    20.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Sun Nov 09 14:08:00 2014 +0100
    20.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Sun Nov 09 17:04:14 2014 +0100
    20.3 @@ -80,7 +80,7 @@
    20.4  fun prove_rhs ctxt def lhs =
    20.5    Old_Z3_Proof_Tools.by_tac ctxt (
    20.6      CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
    20.7 -    THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
    20.8 +    THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI})
    20.9      THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
   20.10  
   20.11  
    21.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Nov 09 14:08:00 2014 +0100
    21.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Nov 09 17:04:14 2014 +0100
    21.3 @@ -412,17 +412,17 @@
    21.4      @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
    21.5      @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
    21.6  
    21.7 -  fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
    21.8 +  fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = (
    21.9      rtac thm ORELSE'
   21.10 -    (match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
   21.11 -    (match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
   21.12 +    (match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE'
   21.13 +    (match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st
   21.14  
   21.15 -  fun nnf_quant_tac_varified vars eq =
   21.16 -    nnf_quant_tac (Old_Z3_Proof_Tools.varify vars eq)
   21.17 +  fun nnf_quant_tac_varified ctxt vars eq =
   21.18 +    nnf_quant_tac ctxt (Old_Z3_Proof_Tools.varify vars eq)
   21.19  
   21.20    fun nnf_quant ctxt vars qs p ct =
   21.21      Old_Z3_Proof_Tools.as_meta_eq ct
   21.22 -    |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified vars (meta_eq_of p) qs)
   21.23 +    |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified ctxt vars (meta_eq_of p) qs)
   21.24  
   21.25    fun prove_nnf ctxt = try_apply ctxt [] [
   21.26      named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq,
   21.27 @@ -555,7 +555,7 @@
   21.28      val thm = meta_eq_of p
   21.29      val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules
   21.30      val cu = Old_Z3_Proof_Tools.as_meta_eq ct
   21.31 -    val tac = REPEAT_ALL_NEW (match_tac rules')
   21.32 +    val tac = REPEAT_ALL_NEW (match_tac ctxt rules')
   21.33    in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end
   21.34  end
   21.35  
   21.36 @@ -577,15 +577,15 @@
   21.37    val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
   21.38    val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
   21.39  
   21.40 -  fun elim_unused_tac i st = (
   21.41 -    match_tac [@{thm refl}]
   21.42 -    ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
   21.43 +  fun elim_unused_tac ctxt i st = (
   21.44 +    match_tac ctxt [@{thm refl}]
   21.45 +    ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
   21.46      ORELSE' (
   21.47 -      match_tac [@{thm iff_allI}, @{thm iff_exI}]
   21.48 -      THEN' elim_unused_tac)) i st
   21.49 +      match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
   21.50 +      THEN' elim_unused_tac ctxt)) i st
   21.51  in
   21.52  
   21.53 -fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt elim_unused_tac
   21.54 +fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (elim_unused_tac ctxt)
   21.55  
   21.56  end
   21.57  
   21.58 @@ -601,7 +601,7 @@
   21.59    val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
   21.60  in
   21.61  fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (
   21.62 -  REPEAT_ALL_NEW (match_tac [rule])
   21.63 +  REPEAT_ALL_NEW (match_tac ctxt [rule])
   21.64    THEN' rtac @{thm excluded_middle})
   21.65  end
   21.66  
    22.1 --- a/src/HOL/NSA/transfer.ML	Sun Nov 09 14:08:00 2014 +0100
    22.2 +++ b/src/HOL/NSA/transfer.ML	Sun Nov 09 17:04:14 2014 +0100
    22.3 @@ -62,10 +62,10 @@
    22.4      val tac =
    22.5        rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
    22.6        ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
    22.7 -      match_tac [transitive_thm] 1 THEN
    22.8 +      match_tac ctxt [transitive_thm] 1 THEN
    22.9        resolve_tac [@{thm transfer_start}] 1 THEN
   22.10        REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
   22.11 -      match_tac [reflexive_thm] 1
   22.12 +      match_tac ctxt [reflexive_thm] 1
   22.13    in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
   22.14  
   22.15  fun transfer_tac ctxt ths =
    23.1 --- a/src/HOL/Nominal/nominal_induct.ML	Sun Nov 09 14:08:00 2014 +0100
    23.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 09 17:04:14 2014 +0100
    23.3 @@ -127,7 +127,7 @@
    23.4                  (rtac (rename_params_rule false [] rule') i THEN
    23.5                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
    23.6      THEN_ALL_NEW_CASES
    23.7 -      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
    23.8 +      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
    23.9          else K all_tac)
   23.10         THEN_ALL_NEW Induct.rulify_tac ctxt)
   23.11    end;
    24.1 --- a/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 14:08:00 2014 +0100
    24.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 17:04:14 2014 +0100
    24.3 @@ -40,8 +40,8 @@
    24.4    val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
    24.5    val safe_best_meson_tac: Proof.context -> int -> tactic
    24.6    val depth_meson_tac: Proof.context -> int -> tactic
    24.7 -  val prolog_step_tac': thm list -> int -> tactic
    24.8 -  val iter_deepen_prolog_tac: thm list -> tactic
    24.9 +  val prolog_step_tac': Proof.context -> thm list -> int -> tactic
   24.10 +  val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic
   24.11    val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
   24.12    val make_meta_clause: thm -> thm
   24.13    val make_meta_clauses: thm list -> thm list
   24.14 @@ -741,17 +741,17 @@
   24.15  
   24.16  (*This version does only one inference per call;
   24.17    having only one eq_assume_tac speeds it up!*)
   24.18 -fun prolog_step_tac' horns =
   24.19 +fun prolog_step_tac' ctxt horns =
   24.20      let val (horn0s, _) = (*0 subgoals vs 1 or more*)
   24.21              take_prefix Thm.no_prems horns
   24.22          val nrtac = net_resolve_tac horns
   24.23      in  fn i => eq_assume_tac i ORELSE
   24.24 -                match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   24.25 +                match_tac ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
   24.26                  ((assume_tac i APPEND nrtac i) THEN check_tac)
   24.27      end;
   24.28  
   24.29 -fun iter_deepen_prolog_tac horns =
   24.30 -    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
   24.31 +fun iter_deepen_prolog_tac ctxt horns =
   24.32 +    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns);
   24.33  
   24.34  fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
   24.35    (fn cls =>
   24.36 @@ -766,7 +766,7 @@
   24.37                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
   24.38          in
   24.39            THEN_ITER_DEEPEN iter_deepen_limit
   24.40 -            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
   24.41 +            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
   24.42          end));
   24.43  
   24.44  fun meson_tac ctxt ths =
    25.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Nov 09 14:08:00 2014 +0100
    25.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Nov 09 17:04:14 2014 +0100
    25.3 @@ -742,7 +742,7 @@
    25.4                THEN rename_tac outer_param_names 1
    25.5                THEN copy_prems_tac (map snd ax_counts) [] 1)
    25.6              THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
    25.7 -            THEN match_tac [prems_imp_false] 1
    25.8 +            THEN match_tac ctxt' [prems_imp_false] 1
    25.9              THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
   25.10                THEN rotate_tac (rotation_of_subgoal i) i
   25.11                THEN PRIMITIVE (unify_first_prem_with_concl thy i)
    26.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Nov 09 14:08:00 2014 +0100
    26.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Nov 09 17:04:14 2014 +0100
    26.3 @@ -471,14 +471,14 @@
    26.4  val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
    26.5  val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
    26.6  
    26.7 -fun elim_unused_tac i st = (
    26.8 -  match_tac [@{thm refl}]
    26.9 -  ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
   26.10 +fun elim_unused_tac ctxt i st = (
   26.11 +  match_tac ctxt [@{thm refl}]
   26.12 +  ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
   26.13    ORELSE' (
   26.14 -    match_tac [@{thm iff_allI}, @{thm iff_exI}]
   26.15 -    THEN' elim_unused_tac)) i st
   26.16 +    match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
   26.17 +    THEN' elim_unused_tac ctxt)) i st
   26.18  
   26.19 -fun elim_unused ctxt _ t = prove ctxt t (fn _ => elim_unused_tac)
   26.20 +fun elim_unused ctxt _ t = prove ctxt t elim_unused_tac
   26.21  
   26.22  
   26.23  (* destructive equality resolution *)
    27.1 --- a/src/HOL/Tools/simpdata.ML	Sun Nov 09 14:08:00 2014 +0100
    27.2 +++ b/src/HOL/Tools/simpdata.ML	Sun Nov 09 17:04:14 2014 +0100
    27.3 @@ -120,9 +120,9 @@
    27.4        reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
    27.5      fun sol_tac i =
    27.6        FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
    27.7 -      (match_tac intros THEN_ALL_NEW sol_tac) i
    27.8 +      (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
    27.9    in
   27.10 -    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
   27.11 +    (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
   27.12    end;
   27.13  
   27.14  val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
   27.15 @@ -130,9 +130,9 @@
   27.16  
   27.17  (*No premature instantiation of variables during simplification*)
   27.18  fun safe_solver_tac ctxt =
   27.19 -  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
   27.20 -  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
   27.21 -    eq_assume_tac, ematch_tac @{thms FalseE}];
   27.22 +  (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN'
   27.23 +  FIRST' [match_tac ctxt (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
   27.24 +    eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
   27.25  
   27.26  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
   27.27  
    28.1 --- a/src/Provers/blast.ML	Sun Nov 09 14:08:00 2014 +0100
    28.2 +++ b/src/Provers/blast.ML	Sun Nov 09 17:04:14 2014 +0100
    28.3 @@ -488,8 +488,8 @@
    28.4  
    28.5  (*Resolution/matching tactics: if upd then the proof state may be updated.
    28.6    Matching makes the tactics more deterministic in the presence of Vars.*)
    28.7 -fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]);
    28.8 -fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]);
    28.9 +fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac ctxt [rl]);
   28.10 +fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac ctxt [rl]);
   28.11  
   28.12  (*Tableau rule from elimination rule.
   28.13    Flag "upd" says that the inference updated the branch.
   28.14 @@ -781,8 +781,8 @@
   28.15  exception PROVE;
   28.16  
   28.17  (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
   28.18 -val contr_tac = ematch_tac [Data.notE] THEN'
   28.19 -                (eq_assume_tac ORELSE' assume_tac);
   28.20 +fun contr_tac ctxt =
   28.21 +  ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac);
   28.22  
   28.23  (*Try to unify complementary literals and return the corresponding tactic. *)
   28.24  fun tryClose state (G, L) =
   28.25 @@ -795,8 +795,8 @@
   28.26    in
   28.27      if isGoal G then close (arg G) L eAssume_tac
   28.28      else if isGoal L then close G (arg L) eAssume_tac
   28.29 -    else if isNot G then close (arg G) L eContr_tac
   28.30 -    else if isNot L then close G (arg L) eContr_tac
   28.31 +    else if isNot G then close (arg G) L (eContr_tac ctxt)
   28.32 +    else if isNot L then close G (arg L) (eContr_tac ctxt)
   28.33      else NONE
   28.34    end;
   28.35  
    29.1 --- a/src/Provers/classical.ML	Sun Nov 09 14:08:00 2014 +0100
    29.2 +++ b/src/Provers/classical.ML	Sun Nov 09 17:04:14 2014 +0100
    29.3 @@ -75,7 +75,7 @@
    29.4    val dup_elim: thm -> thm
    29.5    val dup_intr: thm -> thm
    29.6    val dup_step_tac: Proof.context -> int -> tactic
    29.7 -  val eq_mp_tac: int -> tactic
    29.8 +  val eq_mp_tac: Proof.context -> int -> tactic
    29.9    val haz_step_tac: Proof.context -> int -> tactic
   29.10    val joinrules: thm list * thm list -> (bool * thm) list
   29.11    val mp_tac: int -> tactic
   29.12 @@ -187,7 +187,7 @@
   29.13  fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
   29.14  
   29.15  (*Like mp_tac but instantiates no variables*)
   29.16 -fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
   29.17 +fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
   29.18  
   29.19  (*Creates rules to eliminate ~A, from rules to introduce A*)
   29.20  fun swapify intrs = intrs RLN (2, [Data.swap]);
   29.21 @@ -689,10 +689,14 @@
   29.22  fun ctxt addafter (name, tac2) =
   29.23    ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
   29.24  
   29.25 -fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
   29.26 -fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
   29.27 -fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
   29.28 -fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
   29.29 +fun ctxt addD2 (name, thm) =
   29.30 +  ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
   29.31 +fun ctxt addE2 (name, thm) =
   29.32 +  ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
   29.33 +fun ctxt addSD2 (name, thm) =
   29.34 +  ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac);
   29.35 +fun ctxt addSE2 (name, thm) =
   29.36 +  ctxt addSafter (name, fn ctxt' => ematch_tac ctxt' [thm] THEN' eq_assume_tac);
   29.37  
   29.38  
   29.39  
   29.40 @@ -704,7 +708,7 @@
   29.41      appSWrappers ctxt
   29.42        (FIRST'
   29.43         [eq_assume_tac,
   29.44 -        eq_mp_tac,
   29.45 +        eq_mp_tac ctxt,
   29.46          bimatch_from_nets_tac safe0_netpair,
   29.47          FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
   29.48          bimatch_from_nets_tac safep_netpair])
   29.49 @@ -727,24 +731,24 @@
   29.50  fun n_bimatch_from_nets_tac n =
   29.51    biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
   29.52  
   29.53 -fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i;
   29.54 -val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
   29.55 +fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
   29.56 +fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;
   29.57  
   29.58  (*Two-way branching is allowed only if one of the branches immediately closes*)
   29.59 -fun bimatch2_tac netpair i =
   29.60 +fun bimatch2_tac ctxt netpair i =
   29.61    n_bimatch_from_nets_tac 2 netpair i THEN
   29.62 -  (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
   29.63 +  (eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1));
   29.64  
   29.65  (*Attack subgoals using safe inferences -- matching, not resolution*)
   29.66  fun clarify_step_tac ctxt =
   29.67    let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
   29.68      appSWrappers ctxt
   29.69       (FIRST'
   29.70 -       [eq_assume_contr_tac,
   29.71 +       [eq_assume_contr_tac ctxt,
   29.72          bimatch_from_nets_tac safe0_netpair,
   29.73          FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
   29.74          n_bimatch_from_nets_tac 1 safep_netpair,
   29.75 -        bimatch2_tac safep_netpair])
   29.76 +        bimatch2_tac ctxt safep_netpair])
   29.77    end;
   29.78  
   29.79  fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
    30.1 --- a/src/Provers/hypsubst.ML	Sun Nov 09 14:08:00 2014 +0100
    30.2 +++ b/src/Provers/hypsubst.ML	Sun Nov 09 17:04:14 2014 +0100
    30.3 @@ -223,7 +223,7 @@
    30.4    discarding equalities on Bound variables
    30.5    and on Free variables if thin=true*)
    30.6  fun hyp_subst_tac_thin thin ctxt =
    30.7 -  REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
    30.8 +  REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl],
    30.9      gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
   30.10      if thin then thin_free_eq_tac else K no_tac];
   30.11  
    31.1 --- a/src/Pure/Isar/class_declaration.ML	Sun Nov 09 14:08:00 2014 +0100
    31.2 +++ b/src/Pure/Isar/class_declaration.ML	Sun Nov 09 17:04:14 2014 +0100
    31.3 @@ -94,11 +94,11 @@
    31.4      val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
    31.5      val axclass_intro = #intro (Axclass.get_info thy class);
    31.6      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
    31.7 -    val tac =
    31.8 +    fun tac ctxt =
    31.9        REPEAT (SOMEGOAL
   31.10 -        (match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
   31.11 +        (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
   31.12            ORELSE' assume_tac));
   31.13 -    val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
   31.14 +    val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
   31.15  
   31.16    in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
   31.17  
    32.1 --- a/src/Pure/Isar/method.ML	Sun Nov 09 14:08:00 2014 +0100
    32.2 +++ b/src/Pure/Isar/method.ML	Sun Nov 09 17:04:14 2014 +0100
    32.3 @@ -18,8 +18,8 @@
    32.4    val SIMPLE_METHOD': (int -> tactic) -> method
    32.5    val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
    32.6    val cheating: Proof.context -> bool -> method
    32.7 -  val intro: thm list -> method
    32.8 -  val elim: thm list -> method
    32.9 +  val intro: Proof.context -> thm list -> method
   32.10 +  val elim: Proof.context -> thm list -> method
   32.11    val unfold: thm list -> Proof.context -> method
   32.12    val fold: thm list -> Proof.context -> method
   32.13    val atomize: bool -> Proof.context -> method
   32.14 @@ -127,8 +127,8 @@
   32.15  
   32.16  (* unfold intro/elim rules *)
   32.17  
   32.18 -fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths));
   32.19 -fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths));
   32.20 +fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths));
   32.21 +fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths));
   32.22  
   32.23  
   32.24  (* unfold/fold definitions *)
   32.25 @@ -590,9 +590,9 @@
   32.26      "do nothing (insert current facts only)" #>
   32.27    setup @{binding insert} (Attrib.thms >> (K o insert))
   32.28      "insert theorems, ignoring facts (improper)" #>
   32.29 -  setup @{binding intro} (Attrib.thms >> (K o intro))
   32.30 +  setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
   32.31      "repeatedly apply introduction rules" #>
   32.32 -  setup @{binding elim} (Attrib.thms >> (K o elim))
   32.33 +  setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
   32.34      "repeatedly apply elimination rules" #>
   32.35    setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
   32.36    setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
    33.1 --- a/src/Pure/simplifier.ML	Sun Nov 09 14:08:00 2014 +0100
    33.2 +++ b/src/Pure/simplifier.ML	Sun Nov 09 17:04:14 2014 +0100
    33.3 @@ -389,7 +389,7 @@
    33.4  
    33.5      (*no premature instantiation of variables during simplification*)
    33.6      fun safe_solver_tac ctxt =
    33.7 -      FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
    33.8 +      FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
    33.9      val safe_solver = mk_solver "easy safe" safe_solver_tac;
   33.10  
   33.11      fun mk_eq thm =
    34.1 --- a/src/Pure/tactic.ML	Sun Nov 09 14:08:00 2014 +0100
    34.2 +++ b/src/Pure/tactic.ML	Sun Nov 09 17:04:14 2014 +0100
    34.3 @@ -24,10 +24,10 @@
    34.4    val ftac: thm -> int -> tactic
    34.5    val ares_tac: thm list -> int -> tactic
    34.6    val solve_tac: thm list -> int -> tactic
    34.7 -  val bimatch_tac: (bool * thm) list -> int -> tactic
    34.8 -  val match_tac: thm list -> int -> tactic
    34.9 -  val ematch_tac: thm list -> int -> tactic
   34.10 -  val dmatch_tac: thm list -> int -> tactic
   34.11 +  val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
   34.12 +  val match_tac: Proof.context -> thm list -> int -> tactic
   34.13 +  val ematch_tac: Proof.context -> thm list -> int -> tactic
   34.14 +  val dmatch_tac: Proof.context -> thm list -> int -> tactic
   34.15    val flexflex_tac: Proof.context -> tactic
   34.16    val distinct_subgoal_tac: int -> tactic
   34.17    val distinct_subgoals_tac: tactic
   34.18 @@ -146,10 +146,10 @@
   34.19  fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
   34.20  
   34.21  (*Matching tactics -- as above, but forbid updating of state*)
   34.22 -fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution NONE true brules i);
   34.23 -fun match_tac rules  = bimatch_tac (map (pair false) rules);
   34.24 -fun ematch_tac rules = bimatch_tac (map (pair true) rules);
   34.25 -fun dmatch_tac rls   = ematch_tac (map make_elim rls);
   34.26 +fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i);
   34.27 +fun match_tac ctxt rules = bimatch_tac ctxt (map (pair false) rules);
   34.28 +fun ematch_tac ctxt rules = bimatch_tac ctxt (map (pair true) rules);
   34.29 +fun dmatch_tac ctxt rls = ematch_tac ctxt (map make_elim rls);
   34.30  
   34.31  (*Smash all flex-flex disagreement pairs in the proof state.*)
   34.32  fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt));
    35.1 --- a/src/Sequents/simpdata.ML	Sun Nov 09 14:08:00 2014 +0100
    35.2 +++ b/src/Sequents/simpdata.ML	Sun Nov 09 17:04:14 2014 +0100
    35.3 @@ -62,7 +62,8 @@
    35.4  
    35.5  (*No premature instantiation of variables during simplification*)
    35.6  fun safe_solver ctxt =
    35.7 -  FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ctxt) i), eq_assume_tac];
    35.8 +  FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i),
    35.9 +    eq_assume_tac];
   35.10  
   35.11  (*No simprules, but basic infrastructure for simplification*)
   35.12  val LK_basic_ss =
    36.1 --- a/src/Tools/induct.ML	Sun Nov 09 14:08:00 2014 +0100
    36.2 +++ b/src/Tools/induct.ML	Sun Nov 09 17:04:14 2014 +0100
    36.3 @@ -12,7 +12,7 @@
    36.4    val rulify_fallback: thm list
    36.5    val equal_def: thm
    36.6    val dest_def: term -> (term * term) option
    36.7 -  val trivial_tac: int -> tactic
    36.8 +  val trivial_tac: Proof.context -> int -> tactic
    36.9  end;
   36.10  
   36.11  signature INDUCT =
   36.12 @@ -67,7 +67,7 @@
   36.13    val rulify_tac: Proof.context -> int -> tactic
   36.14    val simplified_rule: Proof.context -> thm -> thm
   36.15    val simplify_tac: Proof.context -> int -> tactic
   36.16 -  val trivial_tac: int -> tactic
   36.17 +  val trivial_tac: Proof.context -> int -> tactic
   36.18    val rotate_tac: int -> int -> int -> tactic
   36.19    val internalize: Proof.context -> int -> thm -> thm
   36.20    val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
   36.21 @@ -513,7 +513,7 @@
   36.22            CASES (Rule_Cases.make_common (thy,
   36.23                Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   36.24              ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
   36.25 -                (if simp then TRY o trivial_tac else K all_tac)) i) st
   36.26 +                (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
   36.27          end)
   36.28    end;
   36.29  
   36.30 @@ -810,7 +810,7 @@
   36.31                      PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
   36.32        end)
   36.33        THEN_ALL_NEW_CASES
   36.34 -        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
   36.35 +        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
   36.36           THEN_ALL_NEW rulify_tac ctxt);
   36.37  
   36.38  val induct_tac = gen_induct_tac (K I);
    37.1 --- a/src/Tools/intuitionistic.ML	Sun Nov 09 14:08:00 2014 +0100
    37.2 +++ b/src/Tools/intuitionistic.ML	Sun Nov 09 17:04:14 2014 +0100
    37.3 @@ -17,13 +17,13 @@
    37.4  
    37.5  local
    37.6  
    37.7 -val remdups_tac = SUBGOAL (fn (g, i) =>
    37.8 +fun remdups_tac ctxt = SUBGOAL (fn (g, i) =>
    37.9    let val prems = Logic.strip_assums_hyp g in
   37.10      REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
   37.11 -    (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
   37.12 +    (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
   37.13    end);
   37.14  
   37.15 -fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
   37.16 +fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
   37.17  
   37.18  val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
   37.19  
   37.20 @@ -39,8 +39,8 @@
   37.21      bires_tac false (Context_Rules.netpair ctxt));
   37.22  
   37.23  fun step_tac ctxt i =
   37.24 -  REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
   37.25 -  REMDUPS (unsafe_step_tac ctxt) i;
   37.26 +  REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
   37.27 +  REMDUPS unsafe_step_tac ctxt i;
   37.28  
   37.29  fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
   37.30    if d > lim then no_tac