diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -170,14 +170,14 @@
    property of the form "... c ... c ... c ..." will lead to a huge unification
    problem, due to the (spurious) choices between projection and imitation. The
    workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
-fun quant_resolve_tac th i st =
+fun quant_resolve_tac ctxt th i st =
   case (concl_of st, prop_of th) of
     (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
     let
       val cc = cterm_of (theory_of_thm th) c
       val ct = Thm.dest_arg (cprop_of th)
-    in resolve_tac [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
-  | _ => resolve_tac [th] i st
+    in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
+  | _ => resolve_tac ctxt [th] i st
 
 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
   e.g. from conj_forward, should have the form
@@ -185,7 +185,7 @@
   and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
 fun forward_res ctxt nf st =
   let
-    fun tacf [prem] = quant_resolve_tac (nf prem) 1
+    fun tacf [prem] = quant_resolve_tac ctxt (nf prem) 1
       | tacf prems =
         error (cat_lines
           ("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
@@ -287,7 +287,7 @@
   case Seq.pull
         (REPEAT
          (Misc_Legacy.METAHYPS ctxt
-           (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1)
+           (fn major::minors => resolve_tac ctxt [nf (minors @ hyps) major] 1) 1)
          st)
   of SOME(th,_) => th
    | NONE => raise THM("forward_res2", 0, [st]);
@@ -390,7 +390,7 @@
                 cnf_nil. The normal form is given to resolve_tac, instantiate a Boolean
                 variable created by resolution with disj_forward. Since (cnf_nil prem)
                 returns a LIST of theorems, we can backtrack to get all combinations.*)
-              let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac (cnf_nil prem) 1) 1
+              let val tac = Misc_Legacy.METAHYPS ctxt (fn [prem] => resolve_tac ctxt (cnf_nil prem) 1) 1
               in  Seq.list_of ((tac THEN tac) (th RS disj_forward)) @ ths  end
           | _ => nodups ctxt th :: ths  (*no work to do*)
       and cnf_nil th = cnf_aux (th, [])
@@ -500,7 +500,7 @@
 
 (* resolve_from_net_tac actually made it slower... *)
 fun prolog_step_tac ctxt horns i =
-    (assume_tac ctxt i APPEND resolve_tac horns i) THEN check_tac THEN
+    (assume_tac ctxt i APPEND resolve_tac ctxt horns i) THEN check_tac THEN
     TRYALL_eq_assume_tac;
 
 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
@@ -698,14 +698,14 @@
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
 
 fun skolemize_prems_tac ctxt prems =
-  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac [exE]
+  cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac ctxt [exE]
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   Function mkcl converts theorems to clauses.*)
 fun MESON preskolem_tac mkcl cltac ctxt i st =
   SELECT_GOAL
     (EVERY [Object_Logic.atomize_prems_tac ctxt 1,
-            resolve_tac @{thms ccontr} 1,
+            resolve_tac ctxt @{thms ccontr} 1,
             preskolem_tac,
             Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
                       EVERY1 [skolemize_prems_tac ctxt negs,
@@ -719,7 +719,7 @@
 fun best_meson_tac sizef ctxt =
   MESON all_tac (make_clauses ctxt)
     (fn cls =>
-         THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
+         THEN_BEST_FIRST (resolve_tac ctxt (gocls cls) 1)
                          (has_fewer_prems 1, sizef)
                          (prolog_step_tac ctxt (make_horns cls) 1))
     ctxt
@@ -732,7 +732,7 @@
 
 fun depth_meson_tac ctxt =
   MESON all_tac (make_clauses ctxt)
-    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)])
+    (fn cls => EVERY [resolve_tac ctxt (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)])
     ctxt
 
 (** Iterative deepening version **)
@@ -764,7 +764,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' ctxt horns)
+            (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
         end));
 
 fun meson_tac ctxt ths =