changeset 2689 | 6d3d893453de |
parent 2630 | 7a962f6829ca |
child 2813 | cc4c816dafdc |
--- a/src/Provers/classical.ML Fri Feb 28 15:46:41 1997 +0100 +++ b/src/Provers/classical.ML Fri Feb 28 15:51:06 1997 +0100 @@ -147,7 +147,7 @@ end; (*Duplication of hazardous rules, for complete provers*) -fun dup_intr th = standard (th RS classical); +fun dup_intr th = zero_var_indexes (th RS classical); fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> rule_by_tactic (TRYALL (etac revcut_rl));