dup_intr & dup_elim no longer call standard -- this
authorpaulson
Fri Feb 28 15:51:06 1997 +0100 (1997-02-28)
changeset 26896d3d893453de
parent 2688 889a1cbd1aca
child 2690 dabe8ab631fa
dup_intr & dup_elim no longer call standard -- this
lets them be used on meta-hyps
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Fri Feb 28 15:46:41 1997 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Feb 28 15:51:06 1997 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4      end;
     1.5  
     1.6  (*Duplication of hazardous rules, for complete provers*)
     1.7 -fun dup_intr th = standard (th RS classical);
     1.8 +fun dup_intr th = zero_var_indexes (th RS classical);
     1.9  
    1.10  fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> 
    1.11                    rule_by_tactic (TRYALL (etac revcut_rl));