| changeset 58950 | d07464875dd4 |
| parent 58838 | 59203adfc33f |
| child 58956 | a816aa3ff391 |
--- a/src/Provers/hypsubst.ML Sat Nov 08 17:39:01 2014 +0100 +++ b/src/Provers/hypsubst.ML Sat Nov 08 21:31:51 2014 +0100 @@ -196,7 +196,7 @@ val imp_intr_tac = resolve_tac [Data.imp_intr]; -fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd; +fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption NONE 2 |> Seq.hd; val dup_subst = rev_dup_elim ssubst (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)