[isabelle-dev] Bind raised in auto

Christian Urban 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 mailing list