diff -r 5c5b5c7f1157 -r a9873318fe30 src/Provers/classical.ML
--- 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 ****)