src/FOL/intprover.ML

--- a/src/FOL/intprover.ML	Sat Apr 27 11:37:50 2013 +0200
+++ b/src/FOL/intprover.ML	Sat Apr 27 20:50:20 2013 +0200
@@ -16,19 +16,19 @@
 *)
 
 signature INT_PROVER = 
-  sig
-  val best_tac: int -> tactic
-  val best_dup_tac: int -> tactic
-  val fast_tac: int -> tactic
+sig
+  val best_tac: Proof.context -> int -> tactic
+  val best_dup_tac: Proof.context -> int -> tactic
+  val fast_tac: Proof.context -> int -> tactic
   val inst_step_tac: int -> tactic
-  val safe_step_tac: 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 step_dup_tac: int -> tactic
+  val safe_tac: Proof.context -> tactic
+  val step_tac: Proof.context -> int -> tactic
+  val step_dup_tac: Proof.context -> int -> tactic
   val haz_brls: (bool * thm) list
   val haz_dup_brls: (bool * thm) list
-  end;
+end;
 
 
 structure IntPr : INT_PROVER   = 
@@ -62,14 +62,16 @@
     List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
 
 (*Attack subgoals using safe inferences -- matching, not resolution*)
-val safe_step_tac = FIRST' [eq_assume_tac,
-                            eq_mp_tac,
-                            bimatch_tac safe0_brls,
-                            hyp_subst_tac,
-                            bimatch_tac safep_brls] ;
+fun safe_step_tac ctxt =
+  FIRST' [
+    eq_assume_tac,
+    eq_mp_tac,
+    bimatch_tac safe0_brls,
+    hyp_subst_tac ctxt,
+    bimatch_tac safep_brls];
 
 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
-val safe_tac = REPEAT_DETERM_FIRST safe_step_tac;
+fun safe_tac ctxt = REPEAT_DETERM_FIRST (safe_step_tac ctxt);
 
 (*These steps could instantiate variables and are therefore unsafe.*)
 val inst_step_tac =
@@ -77,20 +79,20 @@
   biresolve_tac (safe0_brls @ safep_brls);
 
 (*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 i, biresolve_tac haz_brls i];
 
-fun step_dup_tac i = FIRST [safe_tac, inst_step_tac i, biresolve_tac haz_dup_brls i];
+fun step_dup_tac ctxt i = FIRST [safe_tac ctxt, inst_step_tac i, biresolve_tac haz_dup_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));
 
 (*Uses all_dupE: allows multiple use of universal assumptions.  VERY slow.*)
-val best_dup_tac = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac 1));
+fun best_dup_tac ctxt =
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1));
 
 
 end;