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 =