src/FOLP/classical.ML
changeset 59498 50b60f501b05
parent 58963 26bf09b95dda
child 60754 02924903a6fd
     1.1 --- a/src/FOLP/classical.ML	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/FOLP/classical.ML	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -73,7 +73,7 @@
     1.4  fun contr_tac ctxt = etac not_elim THEN'  assume_tac ctxt;
     1.5  
     1.6  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
     1.7 -fun mp_tac ctxt i = eresolve_tac ([not_elim,imp_elim]) i  THEN  assume_tac ctxt i;
     1.8 +fun mp_tac ctxt i = eresolve_tac ctxt ([not_elim,imp_elim]) i  THEN  assume_tac ctxt i;
     1.9  
    1.10  (*Like mp_tac but instantiates no variables*)
    1.11  fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i  THEN  uniq_assume_tac ctxt i;
    1.12 @@ -151,9 +151,9 @@
    1.13  fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) = 
    1.14    FIRST' [uniq_assume_tac ctxt,
    1.15            uniq_mp_tac ctxt,
    1.16 -          biresolve_tac safe0_brls,
    1.17 +          biresolve_tac ctxt safe0_brls,
    1.18            FIRST' hyp_subst_tacs,
    1.19 -          biresolve_tac safep_brls] ;
    1.20 +          biresolve_tac ctxt safep_brls] ;
    1.21  
    1.22  (*Repeatedly attack subgoals using safe inferences*)
    1.23  fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
    1.24 @@ -165,7 +165,7 @@
    1.25  fun step_tac ctxt (cs as (CS{haz_brls,...})) i = 
    1.26    FIRST [safe_tac ctxt cs,
    1.27           inst_step_tac ctxt i,
    1.28 -         biresolve_tac haz_brls i];
    1.29 +         biresolve_tac ctxt haz_brls i];
    1.30  
    1.31  (*** The following tactics all fail unless they solve one goal ***)
    1.32  
    1.33 @@ -179,7 +179,7 @@
    1.34  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
    1.35    allows backtracking from "safe" rules to "unsafe" rules here.*)
    1.36  fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i = 
    1.37 -    safe_tac ctxt cs ORELSE (assume_tac ctxt i APPEND biresolve_tac haz_brls i);
    1.38 +    safe_tac ctxt cs ORELSE (assume_tac ctxt i APPEND biresolve_tac ctxt haz_brls i);
    1.39  
    1.40  end; 
    1.41  end;