src/HOL/Tools/Meson/meson.ML

 (* Special version of "resolve_tac" that works around an explosion in the unifier.
    If the goal has the form "?P c", the danger is that resolving it against a
    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
     "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
   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 [e-mail]:" ::
             Display.string_of_thm ctxt st ::
             "Premises:" :: map (Display.string_of_thm ctxt) prems))

 (*Forward proof, passing extra assumptions as theorems to the tactic*)
 fun forward_res2 ctxt nf hyps st =
   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]);
 
 (*Remove duplicates in P|Q by assuming ~P in Q

                 all combinations of converting P, Q to CNF.*)
               (*There is one assumption, which gets bound to prem and then normalized via
                 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, [])
       val cls =
         if has_too_many_clauses ctxt (concl_of th) then

   then  Seq.empty  else  Seq.single st;
 
 
 (* 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)*)
 fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
 

 
 (*Return all negative clauses, as possible goal clauses*)
 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,
                               Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
   handle THM _ => no_tac st;    (*probably from make_meta_clause, not first-order*)

 
 (*ths is a list of additional clauses (HOL disjunctions) to use.*)
 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
 
 (*First, breaks the goal into independent units*)

 
 (** Depth-first search version **)
 
 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 **)
 
 (*This version does only one inference per call;

             cat_lines ("meson method called:" ::
               map (Display.string_of_thm ctxt) (cls @ ths) @
               ["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 =
   SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (iter_deepen_meson_tac ctxt ths));