[isabelle-dev] Bind raised in auto
urbanc at in.tum.de
Fri Sep 2 13:57:07 CEST 2011
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.
More information about the isabelle-dev