src/Provers/classical.ML
changeset 31945 d5f186aa0bed
parent 30609 983e8b6e4e69
child 32091 30e2ffbba718
     1.1 --- a/src/Provers/classical.ML	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -209,7 +209,7 @@
     1.4  
     1.5  fun dup_elim th =
     1.6      rule_by_tactic (TRYALL (etac revcut_rl))
     1.7 -      ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd);
     1.8 +      ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd);
     1.9  
    1.10  (**** Classical rule sets ****)
    1.11