[isabelle-dev] Bind raised in auto

[Makarius]

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;
       NONE

This indicates a problem in the subgoaler setup, but could be a mistake in 
the check itself, too.


 	Makarius