src/FOLP/intprover.ML

--- a/src/FOLP/intprover.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/FOLP/intprover.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -15,13 +15,13 @@
 
 signature INT_PROVER = 
   sig
-  val best_tac: int -> tactic
-  val fast_tac: int -> tactic
-  val inst_step_tac: int -> tactic
-  val safe_step_tac: int -> tactic
+  val best_tac: Proof.context -> int -> tactic
+  val fast_tac: Proof.context -> int -> tactic
+  val inst_step_tac: Proof.context -> int -> tactic
+  val safe_step_tac: Proof.context -> int -> tactic
   val safe_brls: (bool * thm) list
-  val safe_tac: tactic
-  val step_tac: int -> tactic
+  val safe_tac: Proof.context -> tactic
+  val step_tac: Proof.context -> int -> tactic
   val haz_brls: (bool * thm) list
   end;
 
@@ -52,26 +52,26 @@
     List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
 
 (*Attack subgoals using safe inferences*)
-val safe_step_tac = FIRST' [uniq_assume_tac,
-                            int_uniq_mp_tac,
+fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt,
+                            int_uniq_mp_tac ctxt,
                             biresolve_tac safe0_brls,
                             hyp_subst_tac,
                             biresolve_tac safep_brls] ;
 
 (*Repeatedly attack subgoals using safe inferences*)
-val safe_tac = DETERM (REPEAT_FIRST safe_step_tac);
+fun safe_tac ctxt = DETERM (REPEAT_FIRST (safe_step_tac ctxt));
 
 (*These steps could instantiate variables and are therefore unsafe.*)
-val inst_step_tac = assume_tac APPEND' mp_tac;
+fun inst_step_tac ctxt = assume_tac ctxt APPEND' mp_tac ctxt;
 
 (*One safe or unsafe step. *)
-fun step_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_brls i];
+fun step_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac ctxt i, biresolve_tac haz_brls i];
 
 (*Dumb but fast*)
-val fast_tac = SELECT_GOAL (DEPTH_SOLVE (step_tac 1));
+fun fast_tac ctxt = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
 
 (*Slower but smarter than fast_tac*)
-val best_tac = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
+fun best_tac ctxt =
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
 
 end;