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