src/Tools/intuitionistic.ML
changeset 58957 c9e744ea8a38
parent 58048 aa6296d09e0e
child 58963 26bf09b95dda
--- a/src/Tools/intuitionistic.ML	Sun Nov 09 14:08:00 2014 +0100
+++ b/src/Tools/intuitionistic.ML	Sun Nov 09 17:04:14 2014 +0100
@@ -17,13 +17,13 @@
 
 local
 
-val remdups_tac = SUBGOAL (fn (g, i) =>
+fun remdups_tac ctxt = SUBGOAL (fn (g, i) =>
   let val prems = Logic.strip_assums_hyp g in
     REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
-    (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
+    (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
   end);
 
-fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
+fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
 
 val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
 
@@ -39,8 +39,8 @@
     bires_tac false (Context_Rules.netpair ctxt));
 
 fun step_tac ctxt i =
-  REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
-  REMDUPS (unsafe_step_tac ctxt) i;
+  REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
+  REMDUPS unsafe_step_tac ctxt i;
 
 fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
   if d > lim then no_tac