src/Tools/intuitionistic.ML
changeset 58957 c9e744ea8a38
parent 58048 aa6296d09e0e
child 58963 26bf09b95dda
     1.1 --- a/src/Tools/intuitionistic.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/Tools/intuitionistic.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -17,13 +17,13 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val remdups_tac = SUBGOAL (fn (g, i) =>
     1.8 +fun remdups_tac ctxt = SUBGOAL (fn (g, i) =>
     1.9    let val prems = Logic.strip_assums_hyp g in
    1.10      REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    1.11 -    (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    1.12 +    (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    1.13    end);
    1.14  
    1.15 -fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
    1.16 +fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
    1.17  
    1.18  val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
    1.19  
    1.20 @@ -39,8 +39,8 @@
    1.21      bires_tac false (Context_Rules.netpair ctxt));
    1.22  
    1.23  fun step_tac ctxt i =
    1.24 -  REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
    1.25 -  REMDUPS (unsafe_step_tac ctxt) i;
    1.26 +  REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
    1.27 +  REMDUPS unsafe_step_tac ctxt i;
    1.28  
    1.29  fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
    1.30    if d > lim then no_tac