src/HOL/Tools/Meson/meson.ML

   val abs_extensionalize_conv : Proof.context -> conv
   val abs_extensionalize_thm : Proof.context -> thm -> thm
   val make_clauses_unsorted: Proof.context -> thm list -> thm list
   val make_clauses: Proof.context -> thm list -> thm list
   val make_horns: thm list -> thm list
-  val best_prolog_tac: (thm -> int) -> thm list -> tactic
-  val depth_prolog_tac: thm list -> tactic
+  val best_prolog_tac: Proof.context -> (thm -> int) -> thm list -> tactic
+  val depth_prolog_tac: Proof.context -> thm list -> tactic
   val gocls: thm list -> thm list
   val skolemize_prems_tac : Proof.context -> thm list -> int -> tactic
   val MESON:
     tactic -> (thm list -> thm list) -> (thm list -> tactic) -> Proof.context
     -> int -> tactic

   if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   then  Seq.empty  else  Seq.single st;
 
 
 (* net_resolve_tac actually made it slower... *)
-fun prolog_step_tac horns i =
-    (assume_tac i APPEND resolve_tac horns i) THEN check_tac THEN
+fun prolog_step_tac ctxt horns i =
+    (assume_tac ctxt i APPEND resolve_tac 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;
 

       (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
 
 (*Could simply use nprems_of, which would count remaining subgoals -- no
   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
 
-fun best_prolog_tac sizef horns =
-    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1);
-
-fun depth_prolog_tac horns =
-    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1);
+fun best_prolog_tac ctxt sizef horns =
+    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1);
+
+fun depth_prolog_tac ctxt horns =
+    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1);
 
 (*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 =

 fun best_meson_tac sizef ctxt =
   MESON all_tac (make_clauses ctxt)
     (fn cls =>
          THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
                          (has_fewer_prems 1, sizef)
-                         (prolog_step_tac (make_horns cls) 1))
+                         (prolog_step_tac ctxt (make_horns cls) 1))
     ctxt
 
 (*First, breaks the goal into independent units*)
 fun safe_best_meson_tac ctxt =
   SELECT_GOAL (TRY (safe_tac ctxt) THEN TRYALL (best_meson_tac size_of_subgoals ctxt));
 
 (** 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 (make_horns cls)])
+    (fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac ctxt (make_horns cls)])
     ctxt
 
 (** Iterative deepening version **)
 
 (*This version does only one inference per call;

     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 ctxt horn0s i ORELSE  (*no backtracking if unit MATCHES*)
-                ((assume_tac i APPEND nrtac i) THEN check_tac)
+                ((assume_tac ctxt i APPEND nrtac i) THEN check_tac)
     end;
 
 fun iter_deepen_prolog_tac ctxt horns =
     ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns);