[isabelle-dev] Bind raised in auto

[Christian Urban]

Hi,

I just applied in a proof-script the following tactic

   apply(auto simp add: f_def dest: l3)

and received the error message

   *** exception Bind raised (line 934 of "raw_simplifier.ML")
   *** At command "apply"

Is this supposed to happen?  f_def is from a function 
I defined and l3 is a lemma I proved earlier. Somehow
the problem seems to be connected with the dest.
I can supply the example where it happens. The line
in the raw simplifier is

  val SOME thm'' = check_conv false ss eta_thm thm';

There seems to be a test missing for NONE, but that
is just wild guess work.

Christian