# HG changeset patch
# User paulson
# Date 857141466 -3600
# Node ID 6d3d893453de42eda81f04d884701c00450315f9
# Parent  889a1cbd1aca7ea6332c47d81f421506af321482
dup_intr & dup_elim no longer call standard -- this
lets them be used on meta-hyps

diff -r 889a1cbd1aca -r 6d3d893453de src/Provers/classical.ML
--- 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));