dup_intr & dup_elim no longer call standard -- this
lets them be used on meta-hyps

--- 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));