--- a/src/Provers/classical.ML Fri Apr 30 17:18:29 2010 +0200
+++ b/src/Provers/classical.ML Fri Apr 30 18:06:29 2010 +0200
@@ -208,8 +208,11 @@
fun dup_intr th = zero_var_indexes (th RS classical);
fun dup_elim th =
- rule_by_tactic (TRYALL (etac revcut_rl))
- ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
+ let
+ val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
+ val ctxt = ProofContext.init (Thm.theory_of_thm rl);
+ in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
+
(**** Classical rule sets ****)