[isabelle-dev] Bind raised in auto
makarius at sketis.net
Fri Sep 2 15:41:36 CEST 2011
On Fri, 2 Sep 2011, Christian Urban wrote:
> 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';
The check_conv function also provides some extra trace, if
simp_trace/simp_debug is enabled. See the sources:
trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
trace_term false (fn () => "Should have proved:") ss prop0;
This indicates a problem in the subgoaler setup, but could be a mistake in
the check itself, too.
More information about the isabelle-dev