src/Provers/classical.ML
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));