src/Provers/classical.ML
changeset 36546 a9873318fe30
parent 35625 9c818cab0dd0
child 36610 bafd82950e24
     1.1 --- a/src/Provers/classical.ML	Fri Apr 30 17:18:29 2010 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Apr 30 18:06:29 2010 +0200
     1.3 @@ -208,8 +208,11 @@
     1.4  fun dup_intr th = zero_var_indexes (th RS classical);
     1.5  
     1.6  fun dup_elim th =
     1.7 -    rule_by_tactic (TRYALL (etac revcut_rl))
     1.8 -      ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
     1.9 +  let
    1.10 +    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
    1.11 +    val ctxt = ProofContext.init (Thm.theory_of_thm rl);
    1.12 +  in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end;
    1.13 +
    1.14  
    1.15  (**** Classical rule sets ****)
    1.16