# HG changeset patch
# User wenzelm
# Date 1415549054 -3600
# Node ID c9e744ea8a3815a4d7a6aa3ab6a0ed14b0c0b09d
# Parent  a816aa3ff391152e714a2774729ee29b99ab8f62
proper context for match_tac etc.;

diff -r a816aa3ff391 -r c9e744ea8a38 NEWS
--- a/NEWS	Sun Nov 09 14:08:00 2014 +0100
+++ b/NEWS	Sun Nov 09 17:04:14 2014 +0100
@@ -190,7 +190,7 @@
 
 *** ML ***
 
-* Proper context for various elementary tactics: compose_tac,
+* Proper context for various elementary tactics: match_tac, compose_tac,
 Splitter.split_tac etc.  Minor INCOMPATIBILITY.
 
 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
diff -r a816aa3ff391 -r c9e744ea8a38 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/CCL/Wfd.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -453,10 +453,11 @@
   in IHinst tac @{thms rcallTs} i end
   THEN eresolve_tac @{thms rcall_lemmas} i
 
-fun raw_step_tac ctxt prems i = ares_tac (prems@type_rls) i ORELSE
-                           rcall_tac ctxt i ORELSE
-                           ematch_tac [@{thm SubtypeE}] i ORELSE
-                           match_tac [@{thm SubtypeI}] i
+fun raw_step_tac ctxt prems i =
+  ares_tac (prems@type_rls) i ORELSE
+  rcall_tac ctxt i ORELSE
+  ematch_tac ctxt [@{thm SubtypeE}] i ORELSE
+  match_tac ctxt [@{thm SubtypeI}] i
 
 fun tc_step_tac ctxt prems = SUBGOAL (fn (Bi,i) =>
           if is_rigid_prog Bi then raw_step_tac ctxt prems i else no_tac)
diff -r a816aa3ff391 -r c9e744ea8a38 src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Doc/Implementation/Tactic.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -284,10 +284,10 @@
   @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
   @{index_ML assume_tac: "int -> tactic"} \\
   @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
-  @{index_ML match_tac: "thm list -> int -> tactic"} \\
-  @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
-  @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
-  @{index_ML bimatch_tac: "(bool * thm) list -> int -> tactic"} \\
+  @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
   \end{mldecls}
 
   \begin{description}
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOL/FOL.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -420,7 +420,7 @@
     val rulify_fallback = @{thms induct_rulify_fallback}
     val equal_def = @{thm induct_equal_def}
     fun dest_def _ = NONE
-    fun trivial_tac _ = no_tac
+    fun trivial_tac _ _ = no_tac
   );
 *}
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOL/intprover.ML
--- a/src/FOL/intprover.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOL/intprover.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -66,9 +66,9 @@
   FIRST' [
     eq_assume_tac,
     eq_mp_tac,
-    bimatch_tac safe0_brls,
+    bimatch_tac ctxt safe0_brls,
     hyp_subst_tac ctxt,
-    bimatch_tac safep_brls];
+    bimatch_tac ctxt safep_brls];
 
 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
 fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOL/simpdata.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -113,7 +113,8 @@
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver ctxt =
-  FIRST' [match_tac (triv_rls @ Simplifier.prems_of ctxt), eq_assume_tac, ematch_tac @{thms FalseE}];
+  FIRST' [match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt),
+    eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
 
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss =
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/FOLP.thy
--- a/src/FOLP/FOLP.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/FOLP.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -134,7 +134,7 @@
   "?p2 : ~P | P"
   "?p3 : ~ ~ P <-> P"
   "?p4 : (~P --> P) <-> P"
-  apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})
+  apply (tactic {* ALLGOALS (Cla.fast_tac @{context} FOLP_cs) *})
   done
 
 ML_file "simpdata.ML"
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/classical.ML
--- a/src/FOLP/classical.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/classical.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -44,19 +44,19 @@
       {safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list, 
        safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
        haz_brls: (bool*thm)list}
-  val best_tac : claset -> int -> tactic
+  val best_tac : Proof.context -> claset -> int -> tactic
   val contr_tac : int -> tactic
-  val fast_tac : claset -> int -> tactic
+  val fast_tac : Proof.context -> claset -> int -> tactic
   val inst_step_tac : int -> tactic
   val joinrules : thm list * thm list -> (bool * thm) list
   val mp_tac: int -> tactic
-  val safe_tac : claset -> tactic
-  val safe_step_tac : claset -> int -> tactic
-  val slow_step_tac : claset -> int -> tactic
-  val step_tac : claset -> int -> tactic
+  val safe_tac : Proof.context -> claset -> tactic
+  val safe_step_tac : Proof.context -> claset -> int -> tactic
+  val slow_step_tac : Proof.context -> claset -> int -> tactic
+  val step_tac : Proof.context -> claset -> int -> tactic
   val swapify : thm list -> thm list
   val swap_res_tac : thm list -> int -> tactic
-  val uniq_mp_tac: int -> tactic
+  val uniq_mp_tac: Proof.context -> int -> tactic
   end;
 
 
@@ -76,7 +76,7 @@
 fun mp_tac i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac i;
 
 (*Like mp_tac but instantiates no variables*)
-fun uniq_mp_tac i = ematch_tac ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
+fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac i;
 
 (*Creates rules to eliminate ~A, from rules to introduce A*)
 fun swapify intrs = intrs RLN (2, [swap]);
@@ -148,38 +148,38 @@
 (*** Simple tactics for theorem proving ***)
 
 (*Attack subgoals using safe inferences*)
-fun safe_step_tac (CS{safe0_brls,safep_brls,...}) = 
+fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 
   FIRST' [uniq_assume_tac,
-          uniq_mp_tac,
+          uniq_mp_tac ctxt,
           biresolve_tac safe0_brls,
           FIRST' hyp_subst_tacs,
           biresolve_tac safep_brls] ;
 
 (*Repeatedly attack subgoals using safe inferences*)
-fun safe_tac cs = DETERM (REPEAT_FIRST (safe_step_tac cs));
+fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
 
 (*These steps could instantiate variables and are therefore unsafe.*)
 val inst_step_tac = assume_tac APPEND' contr_tac;
 
 (*Single step for the prover.  FAILS unless it makes progress. *)
-fun step_tac (cs as (CS{haz_brls,...})) i = 
-  FIRST [safe_tac cs,
+fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 
+  FIRST [safe_tac ctxt cs,
          inst_step_tac i,
          biresolve_tac haz_brls i];
 
 (*** The following tactics all fail unless they solve one goal ***)
 
 (*Dumb but fast*)
-fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+fun fast_tac ctxt cs = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt cs 1));
 
 (*Slower but smarter than fast_tac*)
-fun best_tac cs = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
+fun best_tac ctxt cs = 
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1));
 
 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   allows backtracking from "safe" rules to "unsafe" rules here.*)
-fun slow_step_tac (cs as (CS{haz_brls,...})) i = 
-    safe_tac cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
+fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 
+    safe_tac ctxt cs ORELSE (assume_tac i APPEND biresolve_tac haz_brls i);
 
 end; 
 end;
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/Classical.thy
--- a/src/FOLP/ex/Classical.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/Classical.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -10,14 +10,14 @@
 begin
 
 schematic_lemma "?p : (P --> Q | R) --> (P-->Q) | (P-->R)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*If and only if*)
 schematic_lemma "?p : (P<->Q) <-> (Q<->P)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 schematic_lemma "?p : ~ (P <-> ~P)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 
 (*Sample problems from 
@@ -33,134 +33,134 @@
 text "Pelletier's examples"
 (*1*)
 schematic_lemma "?p : (P-->Q)  <->  (~Q --> ~P)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*2*)
 schematic_lemma "?p : ~ ~ P  <->  P"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*3*)
 schematic_lemma "?p : ~(P-->Q) --> (Q-->P)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*4*)
 schematic_lemma "?p : (~P-->Q)  <->  (~Q --> P)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*5*)
 schematic_lemma "?p : ((P|Q)-->(P|R)) --> (P|(Q-->R))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*6*)
 schematic_lemma "?p : P | ~ P"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*7*)
 schematic_lemma "?p : P | ~ ~ ~ P"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*8.  Peirce's law*)
 schematic_lemma "?p : ((P-->Q) --> P)  -->  P"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*9*)
 schematic_lemma "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*10*)
 schematic_lemma "?p : (Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
 schematic_lemma "?p : P<->P"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*12.  "Dijkstra's law"*)
 schematic_lemma "?p : ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*13.  Distributive law*)
 schematic_lemma "?p : P | (Q & R)  <-> (P | Q) & (P | R)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*14*)
 schematic_lemma "?p : (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*15*)
 schematic_lemma "?p : (P --> Q) <-> (~P | Q)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*16*)
 schematic_lemma "?p : (P-->Q) | (Q-->P)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 (*17*)
 schematic_lemma "?p : ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 
 text "Classical Logic: examples with quantifiers"
 
 schematic_lemma "?p : (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 schematic_lemma "?p : (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 schematic_lemma "?p : (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 schematic_lemma "?p : (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 
 text "Problems requiring quantifier duplication"
 
 (*Needs multiple instantiation of ALL.*)
 schematic_lemma "?p : (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 (*Needs double instantiation of the quantifier*)
 schematic_lemma "?p : EX x. P(x) --> P(a) & P(b)"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 schematic_lemma "?p : EX z. P(z) --> (ALL x. P(x))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 
 text "Hard examples with quantifiers"
 
 text "Problem 18"
 schematic_lemma "?p : EX y. ALL x. P(y)-->P(x)"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 19"
 schematic_lemma "?p : EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 20"
 schematic_lemma "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))      
     --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 21"
 schematic_lemma "?p : (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 22"
 schematic_lemma "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 23"
 schematic_lemma "?p : (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 24"
 schematic_lemma "?p : ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &   
      (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))   
     --> (EX x. P(x)&R(x))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 25"
 schematic_lemma "?p : (EX x. P(x)) &  
@@ -174,7 +174,7 @@
 schematic_lemma "?u : ((EX x. p(x)) <-> (EX x. q(x))) &   
      (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   
   --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 27"
 schematic_lemma "?p : (EX x. P(x) & ~Q(x)) &    
@@ -182,49 +182,49 @@
               (ALL x. M(x) & L(x) --> P(x)) &    
               ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))   
           --> (ALL x. M(x) --> ~L(x))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 28.  AMENDED"
 schematic_lemma "?p : (ALL x. P(x) --> (ALL x. Q(x))) &    
         ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &   
         ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))   
     --> (ALL x. P(x) & L(x) --> M(x))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
 schematic_lemma "?p : (EX x. P(x)) & (EX y. Q(y))   
     --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->      
          (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 30"
 schematic_lemma "?p : (ALL x. P(x) | Q(x) --> ~ R(x)) &  
         (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
     --> (ALL x. S(x))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 31"
 schematic_lemma "?p : ~(EX x. P(x) & (Q(x) | R(x))) &  
         (EX x. L(x) & P(x)) &  
         (ALL x. ~ R(x) --> M(x))   
     --> (EX x. L(x) & M(x))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 32"
 schematic_lemma "?p : (ALL x. P(x) & (Q(x)|R(x))-->S(x)) &  
         (ALL x. S(x) & R(x) --> L(x)) &  
         (ALL x. M(x) --> R(x))   
     --> (ALL x. P(x) & M(x) --> L(x))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 33"
 schematic_lemma "?p : (ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->     
      (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 35"
 schematic_lemma "?p : EX x y. P(x,y) -->  (ALL u v. P(u,v))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 36"
 schematic_lemma
@@ -232,7 +232,7 @@
       (ALL x. EX y. G(x,y)) &  
       (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))    
   --> (ALL x. EX y. H(x,y))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 37"
 schematic_lemma "?p : (ALL z. EX w. ALL x. EX y.  
@@ -240,63 +240,63 @@
         (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &  
         ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))   
     --> (ALL x. EX y. R(x,y))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 39"
 schematic_lemma "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 40.  AMENDED"
 schematic_lemma "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
               ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 41"
 schematic_lemma "?p : (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))   
           --> ~ (EX z. ALL x. f(x,z))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 44"
 schematic_lemma "?p : (ALL x. f(x) -->                                     
               (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &        
               (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                    
               --> (EX x. j(x) & ~f(x))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problems (mainly) involving equality or functions"
 
 text "Problem 48"
 schematic_lemma "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 50"
 (*What has this to do with equality?*)
 schematic_lemma "?p : (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 56"
 schematic_lemma
  "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 57"
 schematic_lemma
 "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
       (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 text "Problem 58  NOT PROVED AUTOMATICALLY"
 schematic_lemma
   notes f_cong = subst_context [where t = f]
   shows "?p : (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
-  by (tactic {* fast_tac (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
+  by (tactic {* fast_tac @{context} (FOLP_cs addSIs [@{thm f_cong}]) 1 *})
 
 text "Problem 59"
 schematic_lemma "?p : (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
-  by (tactic "best_tac FOLP_dup_cs 1")
+  by (tactic "best_tac @{context} FOLP_dup_cs 1")
 
 text "Problem 60"
 schematic_lemma "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
-  by (tactic "fast_tac FOLP_cs 1")
+  by (tactic "fast_tac @{context} FOLP_cs 1")
 
 end
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/If.thy
--- a/src/FOLP/ex/If.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/If.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -9,7 +9,7 @@
   assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
   shows "?p : if(P,Q,R)"
 apply (unfold if_def)
-apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
+apply (tactic {* fast_tac @{context} (FOLP_cs addIs @{thms assms}) 1 *})
 done
 
 schematic_lemma ifE:
@@ -19,7 +19,7 @@
   shows "?p : S"
 apply (insert 1)
 apply (unfold if_def)
-apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
+apply (tactic {* fast_tac @{context} (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
 done
 
 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))"
@@ -33,11 +33,11 @@
 ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
 
 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))"
-apply (tactic {* fast_tac if_cs 1 *})
+apply (tactic {* fast_tac @{context} if_cs 1 *})
 done
 
 schematic_lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
-apply (tactic {* fast_tac if_cs 1 *})
+apply (tactic {* fast_tac @{context} if_cs 1 *})
 done
 
 end
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/Intro.thy
--- a/src/FOLP/ex/Intro.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/Intro.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -45,13 +45,13 @@
 
 schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
         -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
-apply (tactic {* fast_tac FOLP_cs 1 *})
+apply (tactic {* fast_tac @{context} FOLP_cs 1 *})
 done
 
 
 schematic_lemma "?p : ALL x. P(x,f(x)) <->
         (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
-apply (tactic {* fast_tac FOLP_cs 1 *})
+apply (tactic {* fast_tac @{context} FOLP_cs 1 *})
 done
 
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/Propositional_Cla.thy
--- a/src/FOLP/ex/Propositional_Cla.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/Propositional_Cla.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -12,106 +12,106 @@
 
 text "commutative laws of & and | "
 schematic_lemma "?p : P & Q  -->  Q & P"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : P | Q  -->  Q | P"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "associative laws of & and | "
 schematic_lemma "?p : (P & Q) & R  -->  P & (Q & R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (P | Q) | R  -->  P | (Q | R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "distributive laws of & and | "
 schematic_lemma "?p : (P & Q) | R  --> (P | R) & (Q | R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (P | R) & (Q | R)  --> (P & Q) | R"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (P | Q) & R  --> (P & R) | (Q & R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 schematic_lemma "?p : (P & R) | (Q & R)  --> (P | Q) & R"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "Laws involving implication"
 
 schematic_lemma "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (P & Q --> R) <-> (P--> (Q-->R))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "Propositions-as-types"
 
 (*The combinator K*)
 schematic_lemma "?p : P --> (Q --> P)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 (*The combinator S*)
 schematic_lemma "?p : (P-->Q-->R)  --> (P-->Q) --> (P-->R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 (*Converse is classical*)
 schematic_lemma "?p : (P-->Q) | (P-->R)  -->  (P --> Q | R)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (P-->Q)  -->  (~Q --> ~P)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "Schwichtenberg's examples (via T. Nipkow)"
 
 schematic_lemma stab_imp: "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma stab_to_peirce: "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
               --> ((P --> Q) --> P) --> P"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma peirce_imp1: "?p : (((Q --> R) --> Q) --> Q)  
                --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
   
 schematic_lemma peirce_imp2: "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma mints: "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma mints_solovev: "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma tatsuta: "?p : (((P7 --> P1) --> P10) --> P4 --> P5)  
           --> (((P8 --> P2) --> P9) --> P3 --> P10)  
           --> (P1 --> P8) --> P6 --> P7  
           --> (((P3 --> P2) --> P9) --> P4)  
           --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma tatsuta1: "?p : (((P8 --> P2) --> P9) --> P3 --> P10)  
      --> (((P3 --> P2) --> P9) --> P4)  
      --> (((P6 --> P1) --> P2) --> P9)  
      --> (((P7 --> P1) --> P10) --> P4 --> P5)  
      --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 end
diff -r a816aa3ff391 -r c9e744ea8a38 src/FOLP/ex/Quantifiers_Cla.thy
--- a/src/FOLP/ex/Quantifiers_Cla.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/FOLP/ex/Quantifiers_Cla.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -11,91 +11,91 @@
 begin
 
 schematic_lemma "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 (*Converse is false*)
 schematic_lemma "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 schematic_lemma "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "Some harder ones"
 
 schematic_lemma "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 (*Converse is false*)
 schematic_lemma "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "Basic test of quantifier reasoning"
 (*TRUE*)
 schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "The following should fail, as they are false!"
 
 schematic_lemma "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
-  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
+  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
   oops
 
 schematic_lemma "?p : (EX x. Q(x))  -->  (ALL x. Q(x))"
-  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
+  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
   oops
 
 schematic_lemma "?p : P(?a) --> (ALL x. P(x))"
-  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
+  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
   oops
 
 schematic_lemma "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
-  apply (tactic {* Cla.fast_tac FOLP_cs 1 *})?
+  apply (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})?
   oops
 
 
 text "Back to things that are provable..."
 
 schematic_lemma "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 (*An example of why exI should be delayed as long as possible*)
 schematic_lemma "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 schematic_lemma "?p : (ALL x. Q(x))  -->  (EX x. Q(x))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 
 text "Some slow ones"
 
 (*Principia Mathematica *11.53  *)
 schematic_lemma "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 (*Principia Mathematica *11.55  *)
 schematic_lemma "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 (*Principia Mathematica *11.61  *)
 schematic_lemma "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
-  by (tactic {* Cla.fast_tac FOLP_cs 1 *})
+  by (tactic {* Cla.fast_tac @{context} FOLP_cs 1 *})
 
 end
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOL.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -1463,7 +1463,7 @@
   val equal_def = @{thm induct_equal_def}
   fun dest_def (Const (@{const_name induct_equal}, _) $ t $ u) = SOME (t, u)
     | dest_def _ = NONE
-  val trivial_tac = match_tac @{thms induct_trueI}
+  fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
 )
 *}
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -148,7 +148,7 @@
       val tr = instantiate' [SOME T, SOME U] [SOME f]
           (mk_meta_eq @{thm Abs_cfun_inverse2});
       val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
-      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)));
+      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac ctxt (rev rules)));
     in SOME (perhaps (SINGLE (tac 1)) tr) end
 *}
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -391,7 +391,6 @@
 
 subsection "input_enabledness and par"
 
-
 (* ugly case distinctions. Heart of proof:
      1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
      2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
@@ -400,7 +399,7 @@
       ==> input_enabled (A||B)"
 apply (unfold input_enabled_def)
 apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac @{theory_context Fun}")
+apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
 apply (simp add: inp_is_act)
 prefer 2
 apply (simp add: inp_is_act)
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Sun Nov 09 17:04:14 2014 +0100
@@ -297,7 +297,8 @@
 fun mkex_induct_tac ctxt sch exA exB =
   EVERY'[Seq_induct_tac ctxt sch defs,
          asm_full_simp_tac ctxt,
-         SELECT_GOAL (safe_tac @{theory_context Fun}),
+         SELECT_GOAL
+          (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
          Seq_case_simp_tac ctxt exA,
          Seq_case_simp_tac ctxt exB,
          asm_full_simp_tac ctxt,
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -151,9 +151,9 @@
       let
         val prop = mk_trp (mk_cont functional)
         val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
-        val tac = REPEAT_ALL_NEW (match_tac (rev rules)) 1
+        fun tac ctxt = REPEAT_ALL_NEW (match_tac ctxt (rev rules)) 1
       in
-        Goal.prove_global thy [] [] prop (K tac)
+        Goal.prove_global thy [] [] prop (tac o #context)
       end
 
     val tuple_unfold_thm =
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -131,7 +131,7 @@
           "The error occurred for the goal statement:\n" ^
           Syntax.string_of_term lthy prop)
         val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
-        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)))
+        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac lthy (rev rules)))
         val slow_tac = SOLVED' (simp_tac lthy)
         val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
       in
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -80,7 +80,7 @@
 fun prove_rhs ctxt def lhs =
   Old_Z3_Proof_Tools.by_tac ctxt (
     CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
-    THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
+    THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI})
     THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
 
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -412,17 +412,17 @@
     @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
     @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
 
-  fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
+  fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = (
     rtac thm ORELSE'
-    (match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
-    (match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
+    (match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE'
+    (match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st
 
-  fun nnf_quant_tac_varified vars eq =
-    nnf_quant_tac (Old_Z3_Proof_Tools.varify vars eq)
+  fun nnf_quant_tac_varified ctxt vars eq =
+    nnf_quant_tac ctxt (Old_Z3_Proof_Tools.varify vars eq)
 
   fun nnf_quant ctxt vars qs p ct =
     Old_Z3_Proof_Tools.as_meta_eq ct
-    |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified vars (meta_eq_of p) qs)
+    |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified ctxt vars (meta_eq_of p) qs)
 
   fun prove_nnf ctxt = try_apply ctxt [] [
     named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq,
@@ -555,7 +555,7 @@
     val thm = meta_eq_of p
     val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules
     val cu = Old_Z3_Proof_Tools.as_meta_eq ct
-    val tac = REPEAT_ALL_NEW (match_tac rules')
+    val tac = REPEAT_ALL_NEW (match_tac ctxt rules')
   in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end
 end
 
@@ -577,15 +577,15 @@
   val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
   val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
 
-  fun elim_unused_tac i st = (
-    match_tac [@{thm refl}]
-    ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+  fun elim_unused_tac ctxt i st = (
+    match_tac ctxt [@{thm refl}]
+    ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
     ORELSE' (
-      match_tac [@{thm iff_allI}, @{thm iff_exI}]
-      THEN' elim_unused_tac)) i st
+      match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
+      THEN' elim_unused_tac ctxt)) i st
 in
 
-fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt elim_unused_tac
+fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (elim_unused_tac ctxt)
 
 end
 
@@ -601,7 +601,7 @@
   val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
 in
 fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (
-  REPEAT_ALL_NEW (match_tac [rule])
+  REPEAT_ALL_NEW (match_tac ctxt [rule])
   THEN' rtac @{thm excluded_middle})
 end
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/NSA/transfer.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -62,10 +62,10 @@
     val tac =
       rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
       ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
-      match_tac [transitive_thm] 1 THEN
+      match_tac ctxt [transitive_thm] 1 THEN
       resolve_tac [@{thm transfer_start}] 1 THEN
       REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
-      match_tac [reflexive_thm] 1
+      match_tac ctxt [reflexive_thm] 1
   in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
 
 fun transfer_tac ctxt ths =
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -127,7 +127,7 @@
                 (rtac (rename_params_rule false [] rule') i THEN
                   PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
     THEN_ALL_NEW_CASES
-      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
+      ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
         else K all_tac)
        THEN_ALL_NEW Induct.rulify_tac ctxt)
   end;
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -40,8 +40,8 @@
   val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
   val safe_best_meson_tac: Proof.context -> int -> tactic
   val depth_meson_tac: Proof.context -> int -> tactic
-  val prolog_step_tac': thm list -> int -> tactic
-  val iter_deepen_prolog_tac: thm list -> tactic
+  val prolog_step_tac': Proof.context -> thm list -> int -> tactic
+  val iter_deepen_prolog_tac: Proof.context -> thm list -> tactic
   val iter_deepen_meson_tac: Proof.context -> thm list -> int -> tactic
   val make_meta_clause: thm -> thm
   val make_meta_clauses: thm list -> thm list
@@ -741,17 +741,17 @@
 
 (*This version does only one inference per call;
   having only one eq_assume_tac speeds it up!*)
-fun prolog_step_tac' horns =
+fun prolog_step_tac' ctxt horns =
     let val (horn0s, _) = (*0 subgoals vs 1 or more*)
             take_prefix Thm.no_prems horns
         val nrtac = net_resolve_tac horns
     in  fn i => eq_assume_tac i ORELSE
-                match_tac horn0s i ORELSE  (*no backtracking if unit MATCHES*)
+                match_tac ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
                 ((assume_tac i APPEND nrtac i) THEN check_tac)
     end;
 
-fun iter_deepen_prolog_tac horns =
-    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
+fun iter_deepen_prolog_tac ctxt horns =
+    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns);
 
 fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
   (fn cls =>
@@ -766,7 +766,7 @@
               ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
         in
           THEN_ITER_DEEPEN iter_deepen_limit
-            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
+            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
         end));
 
 fun meson_tac ctxt ths =
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -742,7 +742,7 @@
               THEN rename_tac outer_param_names 1
               THEN copy_prems_tac (map snd ax_counts) [] 1)
             THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
-            THEN match_tac [prems_imp_false] 1
+            THEN match_tac ctxt' [prems_imp_false] 1
             THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
               THEN rotate_tac (rotation_of_subgoal i) i
               THEN PRIMITIVE (unify_first_prem_with_concl thy i)
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -471,14 +471,14 @@
 val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
 val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
 
-fun elim_unused_tac i st = (
-  match_tac [@{thm refl}]
-  ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+fun elim_unused_tac ctxt i st = (
+  match_tac ctxt [@{thm refl}]
+  ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
   ORELSE' (
-    match_tac [@{thm iff_allI}, @{thm iff_exI}]
-    THEN' elim_unused_tac)) i st
+    match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
+    THEN' elim_unused_tac ctxt)) i st
 
-fun elim_unused ctxt _ t = prove ctxt t (fn _ => elim_unused_tac)
+fun elim_unused ctxt _ t = prove ctxt t elim_unused_tac
 
 
 (* destructive equality resolution *)
diff -r a816aa3ff391 -r c9e744ea8a38 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -120,9 +120,9 @@
       reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
     fun sol_tac i =
       FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
-      (match_tac intros THEN_ALL_NEW sol_tac) i
+      (match_tac ctxt intros THEN_ALL_NEW sol_tac) i
   in
-    (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
+    (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN' sol_tac
   end;
 
 val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac;
@@ -130,9 +130,9 @@
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver_tac ctxt =
-  (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN'
-  FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
-    eq_assume_tac, ematch_tac @{thms FalseE}];
+  (fn i => REPEAT_DETERM (match_tac ctxt @{thms simp_impliesI} i)) THEN'
+  FIRST' [match_tac ctxt (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt),
+    eq_assume_tac, ematch_tac ctxt @{thms FalseE}];
 
 val safe_solver = mk_solver "HOL safe" safe_solver_tac;
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Provers/blast.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -488,8 +488,8 @@
 
 (*Resolution/matching tactics: if upd then the proof state may be updated.
   Matching makes the tactics more deterministic in the presence of Vars.*)
-fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac [rl]);
-fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac [rl]);
+fun emtac ctxt upd rl = TRACE ctxt rl (if upd then eresolve_tac [rl] else ematch_tac ctxt [rl]);
+fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then resolve_tac [rl] else match_tac ctxt [rl]);
 
 (*Tableau rule from elimination rule.
   Flag "upd" says that the inference updated the branch.
@@ -781,8 +781,8 @@
 exception PROVE;
 
 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
-val contr_tac = ematch_tac [Data.notE] THEN'
-                (eq_assume_tac ORELSE' assume_tac);
+fun contr_tac ctxt =
+  ematch_tac ctxt [Data.notE] THEN' (eq_assume_tac ORELSE' assume_tac);
 
 (*Try to unify complementary literals and return the corresponding tactic. *)
 fun tryClose state (G, L) =
@@ -795,8 +795,8 @@
   in
     if isGoal G then close (arg G) L eAssume_tac
     else if isGoal L then close G (arg L) eAssume_tac
-    else if isNot G then close (arg G) L eContr_tac
-    else if isNot L then close G (arg L) eContr_tac
+    else if isNot G then close (arg G) L (eContr_tac ctxt)
+    else if isNot L then close G (arg L) (eContr_tac ctxt)
     else NONE
   end;
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Provers/classical.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -75,7 +75,7 @@
   val dup_elim: thm -> thm
   val dup_intr: thm -> thm
   val dup_step_tac: Proof.context -> int -> tactic
-  val eq_mp_tac: int -> tactic
+  val eq_mp_tac: Proof.context -> int -> tactic
   val haz_step_tac: Proof.context -> int -> tactic
   val joinrules: thm list * thm list -> (bool * thm) list
   val mp_tac: int -> tactic
@@ -187,7 +187,7 @@
 fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
 
 (*Like mp_tac but instantiates no variables*)
-fun eq_mp_tac i = ematch_tac [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
+fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
 
 (*Creates rules to eliminate ~A, from rules to introduce A*)
 fun swapify intrs = intrs RLN (2, [Data.swap]);
@@ -689,10 +689,14 @@
 fun ctxt addafter (name, tac2) =
   ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
 
-fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
-fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
-fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
-fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
+fun ctxt addD2 (name, thm) =
+  ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
+fun ctxt addE2 (name, thm) =
+  ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
+fun ctxt addSD2 (name, thm) =
+  ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac);
+fun ctxt addSE2 (name, thm) =
+  ctxt addSafter (name, fn ctxt' => ematch_tac ctxt' [thm] THEN' eq_assume_tac);
 
 
 
@@ -704,7 +708,7 @@
     appSWrappers ctxt
       (FIRST'
        [eq_assume_tac,
-        eq_mp_tac,
+        eq_mp_tac ctxt,
         bimatch_from_nets_tac safe0_netpair,
         FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
         bimatch_from_nets_tac safep_netpair])
@@ -727,24 +731,24 @@
 fun n_bimatch_from_nets_tac n =
   biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
 
-fun eq_contr_tac i = ematch_tac [Data.not_elim] i THEN eq_assume_tac i;
-val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
+fun eq_contr_tac ctxt i = ematch_tac ctxt [Data.not_elim] i THEN eq_assume_tac i;
+fun eq_assume_contr_tac ctxt = eq_assume_tac ORELSE' eq_contr_tac ctxt;
 
 (*Two-way branching is allowed only if one of the branches immediately closes*)
-fun bimatch2_tac netpair i =
+fun bimatch2_tac ctxt netpair i =
   n_bimatch_from_nets_tac 2 netpair i THEN
-  (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
+  (eq_assume_contr_tac ctxt i ORELSE eq_assume_contr_tac ctxt (i + 1));
 
 (*Attack subgoals using safe inferences -- matching, not resolution*)
 fun clarify_step_tac ctxt =
   let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
     appSWrappers ctxt
      (FIRST'
-       [eq_assume_contr_tac,
+       [eq_assume_contr_tac ctxt,
         bimatch_from_nets_tac safe0_netpair,
         FIRST' (map (fn tac => tac ctxt) Data.hyp_subst_tacs),
         n_bimatch_from_nets_tac 1 safep_netpair,
-        bimatch2_tac safep_netpair])
+        bimatch2_tac ctxt safep_netpair])
   end;
 
 fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
diff -r a816aa3ff391 -r c9e744ea8a38 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Provers/hypsubst.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -223,7 +223,7 @@
   discarding equalities on Bound variables
   and on Free variables if thin=true*)
 fun hyp_subst_tac_thin thin ctxt =
-  REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
+  REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl],
     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
     if thin then thin_free_eq_tac else K no_tac];
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -94,11 +94,11 @@
     val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
     val axclass_intro = #intro (Axclass.get_info thy class);
     val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
-    val tac =
+    fun tac ctxt =
       REPEAT (SOMEGOAL
-        (match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
+        (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
           ORELSE' assume_tac));
-    val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (K tac);
+    val of_class = Goal.prove_sorry_global thy [] [] of_class_prop (tac o #context);
 
   in (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) end;
 
diff -r a816aa3ff391 -r c9e744ea8a38 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/Isar/method.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -18,8 +18,8 @@
   val SIMPLE_METHOD': (int -> tactic) -> method
   val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
   val cheating: Proof.context -> bool -> method
-  val intro: thm list -> method
-  val elim: thm list -> method
+  val intro: Proof.context -> thm list -> method
+  val elim: Proof.context -> thm list -> method
   val unfold: thm list -> Proof.context -> method
   val fold: thm list -> Proof.context -> method
   val atomize: bool -> Proof.context -> method
@@ -127,8 +127,8 @@
 
 (* unfold intro/elim rules *)
 
-fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths));
-fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths));
+fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths));
+fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths));
 
 
 (* unfold/fold definitions *)
@@ -590,9 +590,9 @@
     "do nothing (insert current facts only)" #>
   setup @{binding insert} (Attrib.thms >> (K o insert))
     "insert theorems, ignoring facts (improper)" #>
-  setup @{binding intro} (Attrib.thms >> (K o intro))
+  setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
     "repeatedly apply introduction rules" #>
-  setup @{binding elim} (Attrib.thms >> (K o elim))
+  setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
     "repeatedly apply elimination rules" #>
   setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
   setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>
diff -r a816aa3ff391 -r c9e744ea8a38 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/simplifier.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -389,7 +389,7 @@
 
     (*no premature instantiation of variables during simplification*)
     fun safe_solver_tac ctxt =
-      FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
+      FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
     val safe_solver = mk_solver "easy safe" safe_solver_tac;
 
     fun mk_eq thm =
diff -r a816aa3ff391 -r c9e744ea8a38 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Pure/tactic.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -24,10 +24,10 @@
   val ftac: thm -> int -> tactic
   val ares_tac: thm list -> int -> tactic
   val solve_tac: thm list -> int -> tactic
-  val bimatch_tac: (bool * thm) list -> int -> tactic
-  val match_tac: thm list -> int -> tactic
-  val ematch_tac: thm list -> int -> tactic
-  val dmatch_tac: thm list -> int -> tactic
+  val bimatch_tac: Proof.context -> (bool * thm) list -> int -> tactic
+  val match_tac: Proof.context -> thm list -> int -> tactic
+  val ematch_tac: Proof.context -> thm list -> int -> tactic
+  val dmatch_tac: Proof.context -> thm list -> int -> tactic
   val flexflex_tac: Proof.context -> tactic
   val distinct_subgoal_tac: int -> tactic
   val distinct_subgoals_tac: tactic
@@ -146,10 +146,10 @@
 fun solve_tac rules = resolve_tac rules THEN_ALL_NEW assume_tac;
 
 (*Matching tactics -- as above, but forbid updating of state*)
-fun bimatch_tac brules i = PRIMSEQ (Thm.biresolution NONE true brules i);
-fun match_tac rules  = bimatch_tac (map (pair false) rules);
-fun ematch_tac rules = bimatch_tac (map (pair true) rules);
-fun dmatch_tac rls   = ematch_tac (map make_elim rls);
+fun bimatch_tac ctxt brules i = PRIMSEQ (Thm.biresolution (SOME ctxt) true brules i);
+fun match_tac ctxt rules = bimatch_tac ctxt (map (pair false) rules);
+fun ematch_tac ctxt rules = bimatch_tac ctxt (map (pair true) rules);
+fun dmatch_tac ctxt rls = ematch_tac ctxt (map make_elim rls);
 
 (*Smash all flex-flex disagreement pairs in the proof state.*)
 fun flexflex_tac ctxt = PRIMSEQ (Thm.flexflex_rule (SOME ctxt));
diff -r a816aa3ff391 -r c9e744ea8a38 src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Sequents/simpdata.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -62,7 +62,8 @@
 
 (*No premature instantiation of variables during simplification*)
 fun safe_solver ctxt =
-  FIRST' [fn i => DETERM (match_tac (triv_rls @ Simplifier.prems_of ctxt) i), eq_assume_tac];
+  FIRST' [fn i => DETERM (match_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) i),
+    eq_assume_tac];
 
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss =
diff -r a816aa3ff391 -r c9e744ea8a38 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Tools/induct.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -12,7 +12,7 @@
   val rulify_fallback: thm list
   val equal_def: thm
   val dest_def: term -> (term * term) option
-  val trivial_tac: int -> tactic
+  val trivial_tac: Proof.context -> int -> tactic
 end;
 
 signature INDUCT =
@@ -67,7 +67,7 @@
   val rulify_tac: Proof.context -> int -> tactic
   val simplified_rule: Proof.context -> thm -> thm
   val simplify_tac: Proof.context -> int -> tactic
-  val trivial_tac: int -> tactic
+  val trivial_tac: Proof.context -> int -> tactic
   val rotate_tac: int -> int -> int -> tactic
   val internalize: Proof.context -> int -> thm -> thm
   val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
@@ -513,7 +513,7 @@
           CASES (Rule_Cases.make_common (thy,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
             ((Method.insert_tac more_facts THEN' resolve_tac [rule'] THEN_ALL_NEW
-                (if simp then TRY o trivial_tac else K all_tac)) i) st
+                (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
         end)
   end;
 
@@ -810,7 +810,7 @@
                     PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
       end)
       THEN_ALL_NEW_CASES
-        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
+        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
          THEN_ALL_NEW rulify_tac ctxt);
 
 val induct_tac = gen_induct_tac (K I);
diff -r a816aa3ff391 -r c9e744ea8a38 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Tools/intuitionistic.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -17,13 +17,13 @@
 
 local
 
-val remdups_tac = SUBGOAL (fn (g, i) =>
+fun remdups_tac ctxt = SUBGOAL (fn (g, i) =>
   let val prems = Logic.strip_assums_hyp g in
     REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
-    (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
+    (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
   end);
 
-fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
+fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
 
 val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
 
@@ -39,8 +39,8 @@
     bires_tac false (Context_Rules.netpair ctxt));
 
 fun step_tac ctxt i =
-  REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
-  REMDUPS (unsafe_step_tac ctxt) i;
+  REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
+  REMDUPS unsafe_step_tac ctxt i;
 
 fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
   if d > lim then no_tac