[isabelle-dev] ML tactic for eta-contracting a goal

[Brian Huffman]

Does a simple tactic exist for performing eta-contraction on a goal,
at the ML level?

I need to use explicit eta-contraction in some internal proof scripts
for the HOLCF fixrec package, to avoid the weird interactions with
eta-contraction and simplifier congruence rules that I have complained
about recently.

I found that "apply (subst refl)" will eta-contract the current goal,
and so currently I am using the following function which does the ML
equivalent:

fun eta_tac (ctxt : Proof.context) : int -> tactic =
  EqSubst.eqsubst_tac ctxt [0] @{thms refl};

But this code is far from self-explanatory, and it seems like there
must be a simpler, more direct way to do this. In particular, it
doesn't seem like eta_tac should need to take a Proof.context as an
argument.

- Brian