src/Provers/classical.ML

--- a/src/Provers/classical.ML	Sun Nov 09 20:49:28 2014 +0100
+++ b/src/Provers/classical.ML	Mon Nov 10 21:49:48 2014 +0100
@@ -71,14 +71,14 @@
   val depth_tac: Proof.context -> int -> int -> tactic
   val deepen_tac: Proof.context -> int -> int -> tactic
 
-  val contr_tac: int -> tactic
+  val contr_tac: Proof.context -> int -> tactic
   val dup_elim: Context.generic option -> thm -> thm
   val dup_intr: thm -> thm
   val dup_step_tac: Proof.context -> int -> tactic
   val eq_mp_tac: Proof.context -> int -> tactic
   val haz_step_tac: Proof.context -> int -> tactic
   val joinrules: thm list * thm list -> (bool * thm) list
-  val mp_tac: int -> tactic
+  val mp_tac: Proof.context -> int -> tactic
   val safe_tac: Proof.context -> tactic
   val safe_steps_tac: Proof.context -> int -> tactic
   val safe_step_tac: Proof.context -> int -> tactic
@@ -87,7 +87,7 @@
   val step_tac: Proof.context -> int -> tactic
   val slow_step_tac: Proof.context -> int -> tactic
   val swapify: thm list -> thm list
-  val swap_res_tac: thm list -> int -> tactic
+  val swap_res_tac: Proof.context -> thm list -> int -> tactic
   val inst_step_tac: Proof.context -> int -> tactic
   val inst0_step_tac: Proof.context -> int -> tactic
   val instp_step_tac: Proof.context -> int -> tactic
@@ -179,12 +179,12 @@
 (*Prove goal that assumes both P and ~P.
   No backtracking if it finds an equal assumption.  Perhaps should call
   ematch_tac instead of eresolve_tac, but then cannot prove ZF/cantor.*)
-val contr_tac =
-  eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac);
+fun contr_tac ctxt =
+  eresolve_tac [Data.not_elim] THEN' (eq_assume_tac ORELSE' assume_tac ctxt);
 
 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   Could do the same thing for P<->Q and P... *)
-fun mp_tac i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac i;
+fun mp_tac ctxt i = eresolve_tac [Data.not_elim, Data.imp_elim] i THEN assume_tac ctxt i;
 
 (*Like mp_tac but instantiates no variables*)
 fun eq_mp_tac ctxt i = ematch_tac ctxt [Data.not_elim, Data.imp_elim] i THEN eq_assume_tac i;
@@ -195,10 +195,10 @@
 
 (*Uses introduction rules in the normal way, or on negated assumptions,
   trying rules in order. *)
-fun swap_res_tac rls =
+fun swap_res_tac ctxt rls =
   let fun addrl rl brls = (false, rl) :: (true, rl RSN (2, Data.swap)) :: brls in
-    assume_tac ORELSE'
-    contr_tac ORELSE'
+    assume_tac ctxt ORELSE'
+    contr_tac ctxt ORELSE'
     biresolve_tac (fold_rev addrl rls [])
   end;
 
@@ -693,9 +693,9 @@
   ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
 
 fun ctxt addD2 (name, thm) =
-  ctxt addafter (name, fn _ => dresolve_tac [thm] THEN' assume_tac);
+  ctxt addafter (name, fn ctxt' => dresolve_tac [thm] THEN' assume_tac ctxt');
 fun ctxt addE2 (name, thm) =
-  ctxt addafter (name, fn _ => eresolve_tac [thm] THEN' assume_tac);
+  ctxt addafter (name, fn ctxt' => eresolve_tac [thm] THEN' assume_tac ctxt');
 fun ctxt addSD2 (name, thm) =
   ctxt addSafter (name, fn ctxt' => dmatch_tac ctxt' [thm] THEN' eq_assume_tac);
 fun ctxt addSE2 (name, thm) =
@@ -762,8 +762,8 @@
 (*Backtracking is allowed among the various these unsafe ways of
   proving a subgoal.  *)
 fun inst0_step_tac ctxt =
-  assume_tac APPEND'
-  contr_tac APPEND'
+  assume_tac ctxt APPEND'
+  contr_tac ctxt APPEND'
   biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
 
 (*These unsafe steps could generate more subgoals.*)